From 622f9bc866dce734f69444abad21fa7c515321fe Mon Sep 17 00:00:00 2001 From: Juan Marin Noguera Date: Tue, 6 Sep 2022 17:17:23 +0200 Subject: Actualizado README --- README.md | 24 +- fli/n.lyx | 253 ++++++++++ fli/n1.lyx | 346 +++++++++++++ fli/n2.lyx | 1518 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ fli/n3.lyx | 1512 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ fli/n4.lyx | 402 ++++++++++++++++ fli/n5.lyx | 660 +++++++++++++++++++++++++ fli/n6.lyx | 1406 +++++++++++++++++++++++++++++++++++++++++++++++++++++ fli/n7.lyx | 609 +++++++++++++++++++++++ logic/n.lyx | 253 ---------- logic/n1.lyx | 346 ------------- logic/n2.lyx | 1518 ---------------------------------------------------------- logic/n3.lyx | 1512 --------------------------------------------------------- logic/n4.lyx | 402 ---------------- logic/n5.lyx | 660 ------------------------- logic/n6.lyx | 1406 ----------------------------------------------------- logic/n7.lyx | 609 ----------------------- si/n3.lyx | 51 +- 18 files changed, 6762 insertions(+), 6725 deletions(-) create mode 100644 fli/n.lyx create mode 100644 fli/n1.lyx create mode 100644 fli/n2.lyx create mode 100644 fli/n3.lyx create mode 100644 fli/n4.lyx create mode 100644 fli/n5.lyx create mode 100644 fli/n6.lyx create mode 100644 fli/n7.lyx delete mode 100644 logic/n.lyx delete mode 100644 logic/n1.lyx delete mode 100644 logic/n2.lyx delete mode 100644 logic/n3.lyx delete mode 100644 logic/n4.lyx delete mode 100644 logic/n5.lyx delete mode 100644 logic/n6.lyx delete mode 100644 logic/n7.lyx diff --git a/README.md b/README.md index e93004a..2477297 100644 --- a/README.md +++ b/README.md @@ -31,10 +31,15 @@ Se incluyen las siguientes asignaturas: * `ga`: Grupos y Anillos. * `ts`: Topología de Superficies. * `fvc`: Funciones de Variable Compleja (falta la primera parte). + * `gcs`: Geometría de Curvas y Superficies. + * `ggs`: Geometría Global de Superficies. + * `graf`: Grafos y Optimización Discreta. + * `mne`: Métodos Numéricos de las Ecuaciones Diferenciales. + * `ealg`: Ecuaciones algebraicas. * De informática: * `fc`: Fundamentos de Computadores. * `ip`: Introducción a la Programación. - * `logic`: Fundamentos Lógicos de la Informática. + * `fli`: Fundamentos Lógicos de la Informática. * `etc`: Estructura y Tecnología de Computadores. * `ffi`: Fundamentos Físicos de la Informática. * `tp`: Tecnología de la Programación. @@ -49,21 +54,24 @@ Se incluyen las siguientes asignaturas: * `cc`: Compiladores. * `ar`: Ampliación de Redes (sólo PDF). * `st`: Servicios Telemáticos. - -Próximamente: * `aoc`: Arquitectura y Organización de Computadores. - * `gcs`: Geometría de Curvas y Superficies. - * `graf`: Grafos y Optimización Discreta. - * `mne`: Métodos Numéricos de las Ecuaciones Diferenciales. * `si`: Sistemas Inteligentes. * `tds`: Tecnologías de Desarrollo de Software. + * `pds`: Procesos de Desarrollo de Software. + * `gpds`: Gestión de Proyectos de Desarrollo de Software. +* En progreso: + * `ac`: Álgebra Conmutativa. + * `af`: Análisis Funcional. + * `dsi`: Desarrollo de Sistemas Inteligentes. + * `mc`: Modelos de Computación. + * `pia`: Programación para la IA. ## Venta benéfica Si está en Murcia, puede comprar versiones impresas de los apuntes (ver imagen) por un mínimo de 5 euros la asignatura o 19 euros por 6 asignaturas, y **el 100% de los beneficios** se destina a -[Project Elea](https://projectelea.org/about-us/), un grupo de voluntarios que -trabajan con los residentes del campo de refugiados de Eleonas, Grecia, para +**[Project Elea](https://projectelea.org/about-us/)**, un grupo de voluntarios +que trabajan con los residentes del campo de refugiados de Eleonas, Grecia, para mejorar los estándares de vida y el bienestar comunitario de estas personas que han perdido todo a causa de la guerra. diff --git a/fli/n.lyx b/fli/n.lyx new file mode 100644 index 0000000..57fe1dd --- /dev/null +++ b/fli/n.lyx @@ -0,0 +1,253 @@ +#LyX 2.3 created this file. For more info see http://www.lyx.org/ +\lyxformat 544 +\begin_document +\begin_header +\save_transient_properties true +\origin unavailable +\textclass book +\use_default_options true +\maintain_unincluded_children false +\language spanish +\language_package default +\inputencoding auto +\fontencoding global +\font_roman "default" "default" +\font_sans "default" "default" +\font_typewriter "default" "default" +\font_math "auto" "auto" +\font_default_family default +\use_non_tex_fonts false +\font_sc false +\font_osf false +\font_sf_scale 100 100 +\font_tt_scale 100 100 +\use_microtype false +\use_dash_ligatures true +\graphics default +\default_output_format default +\output_sync 0 +\bibtex_command default +\index_command default +\paperfontsize default +\spacing single +\use_hyperref false +\papersize a5paper +\use_geometry true +\use_package amsmath 1 +\use_package amssymb 1 +\use_package cancel 1 +\use_package esint 1 +\use_package mathdots 1 +\use_package mathtools 1 +\use_package mhchem 1 +\use_package stackrel 1 +\use_package stmaryrd 1 +\use_package undertilde 1 +\cite_engine basic +\cite_engine_type default +\biblio_style plain +\use_bibtopic false +\use_indices false +\paperorientation portrait +\suppress_date false +\justification true +\use_refstyle 1 +\use_minted 0 +\index Index +\shortcut idx +\color #008000 +\end_index +\leftmargin 0.2cm +\topmargin 0.7cm +\rightmargin 0.2cm +\bottommargin 0.7cm +\secnumdepth 3 +\tocdepth 3 +\paragraph_separation indent +\paragraph_indentation default +\is_math_indent 0 +\math_numbering_side default +\quotes_style swiss +\dynamic_quotes 0 +\papercolumns 1 +\papersides 1 +\paperpagestyle empty +\tracking_changes false +\output_changes false +\html_math_output 0 +\html_css_as_file 0 +\html_be_strict false +\end_header + +\begin_body + +\begin_layout Title +Fundamentos Lógicos de la Informática +\end_layout + +\begin_layout Date +\begin_inset Note Note +status open + +\begin_layout Plain Layout + +\end_layout + +\end_inset + + +\end_layout + +\begin_layout Standard +\begin_inset ERT +status open + +\begin_layout Plain Layout + + +\backslash +def +\backslash +cryear{2017} +\end_layout + +\end_inset + + +\end_layout + +\begin_layout Standard +\begin_inset CommandInset include +LatexCommand input +filename "../license.lyx" + +\end_inset + + +\end_layout + +\begin_layout Standard +Bibliografía: +\end_layout + +\begin_layout Itemize +Diapositivas de Fundamentos Lógicos de la Informática, Departamento de Ingenierí +a de al Información y las Comunicaciones (nota: la errata es de ellos), + Facultad de Informática, Universidad de Murcia. +\end_layout + +\begin_layout Itemize +Wikipedia, la enciclopedia libre ( +\begin_inset Flex URL +status open + +\begin_layout Plain Layout + +https://es.wikipedia.org/ +\end_layout + +\end_inset + +). +\end_layout + +\begin_layout Chapter +Lógica +\end_layout + +\begin_layout Standard +\begin_inset CommandInset include +LatexCommand input +filename "n1.lyx" + +\end_inset + + +\end_layout + +\begin_layout Chapter +Lógica proposicional +\end_layout + +\begin_layout Standard +\begin_inset CommandInset include +LatexCommand input +filename "n2.lyx" + +\end_inset + + +\end_layout + +\begin_layout Chapter +Problema SAT +\end_layout + +\begin_layout Standard +\begin_inset CommandInset include +LatexCommand input +filename "n3.lyx" + +\end_inset + + +\end_layout + +\begin_layout Chapter +Deducción natural +\end_layout + +\begin_layout Standard +\begin_inset CommandInset include +LatexCommand input +filename "n4.lyx" + +\end_inset + + +\end_layout + +\begin_layout Chapter +Lógica categórica +\end_layout + +\begin_layout Standard +\begin_inset CommandInset include +LatexCommand input +filename "n5.lyx" + +\end_inset + + +\end_layout + +\begin_layout Chapter +Lógica de predicados de primer orden +\end_layout + +\begin_layout Standard +\begin_inset CommandInset include +LatexCommand input +filename "n6.lyx" + +\end_inset + + +\end_layout + +\begin_layout Chapter +Sistemas deductivos, razonamientos y deducciones +\end_layout + +\begin_layout Standard +\begin_inset CommandInset include +LatexCommand input +filename "n7.lyx" + +\end_inset + + +\end_layout + +\end_body +\end_document diff --git a/fli/n1.lyx b/fli/n1.lyx new file mode 100644 index 0000000..166b2b3 --- /dev/null +++ b/fli/n1.lyx @@ -0,0 +1,346 @@ +#LyX 2.3 created this file. For more info see http://www.lyx.org/ +\lyxformat 544 +\begin_document +\begin_header +\save_transient_properties true +\origin unavailable +\textclass book +\use_default_options true +\maintain_unincluded_children false +\language spanish +\language_package default +\inputencoding auto +\fontencoding global +\font_roman "default" "default" +\font_sans "default" "default" +\font_typewriter "default" "default" +\font_math "auto" "auto" +\font_default_family default +\use_non_tex_fonts false +\font_sc false +\font_osf false +\font_sf_scale 100 100 +\font_tt_scale 100 100 +\use_microtype false +\use_dash_ligatures true +\graphics default +\default_output_format default +\output_sync 0 +\bibtex_command default +\index_command default +\paperfontsize default +\spacing single +\use_hyperref false +\papersize default +\use_geometry false +\use_package amsmath 1 +\use_package amssymb 1 +\use_package cancel 1 +\use_package esint 1 +\use_package mathdots 1 +\use_package mathtools 1 +\use_package mhchem 1 +\use_package stackrel 1 +\use_package stmaryrd 1 +\use_package undertilde 1 +\cite_engine basic +\cite_engine_type default +\biblio_style plain +\use_bibtopic false +\use_indices false +\paperorientation portrait +\suppress_date false +\justification true +\use_refstyle 1 +\use_minted 0 +\index Index +\shortcut idx +\color #008000 +\end_index +\secnumdepth 3 +\tocdepth 3 +\paragraph_separation indent +\paragraph_indentation default +\is_math_indent 0 +\math_numbering_side default +\quotes_style swiss +\dynamic_quotes 0 +\papercolumns 1 +\papersides 1 +\paperpagestyle default +\tracking_changes false +\output_changes false +\html_math_output 0 +\html_css_as_file 0 +\html_be_strict false +\end_header + +\begin_body + +\begin_layout Standard +La lógica estudia las oraciones y los razonamientos, y existen tantas como + tipos de oraciones y razonamientos. + En informática, es la base de la programación, representa el conocimiento + en inteligencia artificial, sirve para demostraciones de resultados teóricos + y diseño de circuitos lógicos y define los problemas NP-completos (SAT). + Existen distintas lógicas, como las lógicas clásicas (proposicional, categórica +, de primer orden...) y la lógica difusa. +\end_layout + +\begin_layout Section +Oraciones +\end_layout + +\begin_layout Standard +Dentro de una misma lógica, una oración lógica es una oración del lenguaje + natural que cumpla ciertas condiciones. + En las lógicas clásicas, es aquella que es +\series bold +enunciativa +\series default + y cumple la +\series bold +ley del tercero excluido +\series default + (solo puede ser verdadera [ +\begin_inset Formula $V$ +\end_inset + +] o falsa [ +\begin_inset Formula $F$ +\end_inset + +]) y la +\series bold +ley de no contradicción +\series default + (no puede ser +\begin_inset Formula $V$ +\end_inset + + y +\begin_inset Formula $F$ +\end_inset + + a la vez). + Estas pueden ser +\series bold +simples +\series default + ( +\series bold +atómicas +\series default +) o +\series bold +compuestas +\series default + ( +\series bold +moleculares +\series default +), dependiendo de si tienen uno o más predicados. +\end_layout + +\begin_layout Section +Razonamientos +\end_layout + +\begin_layout Standard +Un razonamiento es una estructura que enlaza oraciones, de las cuales una + es la +\series bold +conclusión +\series default + de otras ( +\series bold +premisas +\series default +) y todas (salvo ella misma) proporcionan evidencias para justificarla. + Así, un razonamiento está formado por +\series bold +axiomas +\series default + o +\series bold +premisas +\series default +; +\series bold +conclusiones +\series default + o +\series bold +teoremas +\series default +, y una +\series bold +demostración +\series default +. + Existen dos tipos de razonamiento: +\end_layout + +\begin_layout Itemize + +\series bold +Deductivo: +\series default + Se basa en la implicación. +\end_layout + +\begin_layout Itemize + +\series bold +Inductivo: +\series default + Parte de casos y llega a una conclusión general. + Sólo es válido si se consideran todos los casos; de lo contrario la conclusión + es probablemente, pero no necesariamente, cierta. +\end_layout + +\begin_layout Standard +Un razonamiento es válido si la conclusión es necesariamente cierta cuando + lo son las premisas, y se escribe como +\begin_inset Formula $\underset{\text{Premisas}}{\{\alpha_{1},\alpha_{2},\dots,\alpha_{n}\}}\vDash\underset{\text{Conclusión}}{\beta}$ +\end_inset + +. + Para representarlo: +\end_layout + +\begin_layout Itemize + +\series bold +Representación gráfica: +\series default + +\begin_inset Formula +\[ +\begin{array}{ccccc} +P_{1} & \land & P_{2}\\ +\hline & \downarrow\\ + & C_{1} & & \land & P_{3}\\ +\hline & & & \downarrow\\ + & & & C_{2} +\end{array} +\] + +\end_inset + + +\end_layout + +\begin_layout Itemize + +\series bold +Representación estándar: +\begin_inset Formula +\[ +\begin{array}{ccc} + & P_{1}\\ + & P_{2}\\ +\hline \therefore & C_{1} & P_{1}\text{ y }P_{2}\\ + & P_{3}\\ +\hline \therefore & C_{2} & C_{1}\text{ y }P_{3} +\end{array} +\] + +\end_inset + + +\end_layout + +\begin_layout Section +Tipos de definiciones +\end_layout + +\begin_layout Itemize + +\series bold +Extensiva +\series default + o +\series bold +extensional: +\series default + Lista de elementos que cumplen la condición. +\end_layout + +\begin_layout Itemize + +\series bold +Comprensiva +\series default + o +\series bold +intensional: +\series default + Lista de propiedades necesarias. +\end_layout + +\begin_layout Itemize + +\series bold +Recursiva: +\series default + Formada por una +\series bold +regla base +\series default +, que define casos concretos, y una +\series bold +regla recursiva +\series default +, que define todos los demás casos a partir de casos ya conocidos mediante + una relación. + También puede contener una +\series bold +regla de exclusión +\series default +. +\end_layout + +\begin_layout Section +Lenguajes formales +\end_layout + +\begin_layout Standard +El lenguaje natural es ambiguo, y suele ser vago, paradójico, complicado... + Por tanto, en ciencia es imprescindible un lenguaje formal para obtener + rigor. + Un lenguaje formal consta de un conjunto de símbolos ( +\series bold +alfabeto +\series default + o +\series bold +vocabulario +\series default +) y una definición recursiva para conectarlos ( +\series bold +gramática +\series default + o +\series bold +sintaxis +\series default +), y es el conjunto de todas las fórmulas bien formadas (f.b.f.) obtenidas + a partir de estas. + En la práctica, necesitamos un sistema de codificación (formalización) + y de interpretación. +\end_layout + +\begin_layout Section +Formalización e interpretación +\end_layout + +\begin_layout Standard +Formalizar es obtener una oración o f.b.f. + en lenguaje formal a partir del lenguaje natural, mientras que interpretar + es entender una f.b.f. + expresándola en lenguaje natural. +\end_layout + +\end_body +\end_document diff --git a/fli/n2.lyx b/fli/n2.lyx new file mode 100644 index 0000000..93478b7 --- /dev/null +++ b/fli/n2.lyx @@ -0,0 +1,1518 @@ +#LyX 2.3 created this file. For more info see http://www.lyx.org/ +\lyxformat 544 +\begin_document +\begin_header +\save_transient_properties true +\origin unavailable +\textclass book +\use_default_options true +\maintain_unincluded_children false +\language spanish +\language_package default +\inputencoding auto +\fontencoding global +\font_roman "default" "default" +\font_sans "default" "default" +\font_typewriter "default" "default" +\font_math "auto" "auto" +\font_default_family default +\use_non_tex_fonts false +\font_sc false +\font_osf false +\font_sf_scale 100 100 +\font_tt_scale 100 100 +\use_microtype false +\use_dash_ligatures true +\graphics default +\default_output_format default +\output_sync 0 +\bibtex_command default +\index_command default +\paperfontsize default +\spacing single +\use_hyperref false +\papersize default +\use_geometry false +\use_package amsmath 1 +\use_package amssymb 1 +\use_package cancel 1 +\use_package esint 1 +\use_package mathdots 1 +\use_package mathtools 1 +\use_package mhchem 1 +\use_package stackrel 1 +\use_package stmaryrd 1 +\use_package undertilde 1 +\cite_engine basic +\cite_engine_type default +\biblio_style plain +\use_bibtopic false +\use_indices false +\paperorientation portrait +\suppress_date false +\justification true +\use_refstyle 1 +\use_minted 0 +\index Index +\shortcut idx +\color #008000 +\end_index +\secnumdepth 3 +\tocdepth 3 +\paragraph_separation indent +\paragraph_indentation default +\is_math_indent 0 +\math_numbering_side default +\quotes_style swiss +\dynamic_quotes 0 +\papercolumns 1 +\papersides 1 +\paperpagestyle default +\tracking_changes false +\output_changes false +\html_math_output 0 +\html_css_as_file 0 +\html_be_strict false +\end_header + +\begin_body + +\begin_layout Standard +Las oraciones lógicas en lógica proposicional ( +\series bold +L0 +\series default +) se llaman +\series bold +proposiciones +\series default +. + Las proposiciones atómicas, también llamadas +\series bold +sentencias +\series default + o +\series bold +átomos +\series default +, se agrupan mediante +\series bold +operadores lógicos +\series default + para formar oraciones compuestas. +\end_layout + +\begin_layout Section +Sintaxis +\end_layout + +\begin_layout Itemize + +\series bold +Constantes: +\series default + Verdadero ( +\begin_inset Formula $V$ +\end_inset + +) o falso ( +\begin_inset Formula $F$ +\end_inset + +). + +\begin_inset Formula $\mathbb{B}=\{V,F\}$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Sentencias: +\series default + Se representan por un conjunto de letras latinas. + El conjunto de todos se denota por +\begin_inset Formula ${\cal P}$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Operadores lógicos: +\series default + Negación ( +\begin_inset Formula $\neg$ +\end_inset + +) y conectivos. + Los conectivos son: conjunción ( +\begin_inset Formula $\land$ +\end_inset + +), disyunción ( +\begin_inset Formula $\lor$ +\end_inset + +), implicación ( +\begin_inset Formula $\rightarrow$ +\end_inset + +) y doble implicación ( +\begin_inset Formula $\leftrightarrow$ +\end_inset + +). +\end_layout + +\begin_layout Itemize + +\series bold +Paréntesis +\series default + o corchetes, para agrupar expresiones. +\end_layout + +\begin_layout Standard +Definición recursiva de una f.b.f.: +\end_layout + +\begin_layout Itemize + +\series bold +Forma básica: +\series default + Todo átomo es una f.b.f. +\end_layout + +\begin_layout Itemize + +\series bold +Forma recursiva: +\series default + Si +\begin_inset Formula $\alpha$ +\end_inset + + y +\begin_inset Formula $\beta$ +\end_inset + + son f.b.f., también lo son +\begin_inset Formula $\neg\alpha$ +\end_inset + +, +\begin_inset Formula $(\alpha\land\beta)$ +\end_inset + +, +\begin_inset Formula $(\alpha\lor\beta)$ +\end_inset + +, +\begin_inset Formula $(\alpha\rightarrow\beta)$ +\end_inset + + y +\begin_inset Formula $(\alpha\leftrightarrow\beta)$ +\end_inset + +. + La presencia o ausencia de paréntesis es importante. +\end_layout + +\begin_layout Standard +En la práctica, podemos eliminar paréntesis según estas reglas: +\end_layout + +\begin_layout Itemize +Se pueden eliminar los paréntesis exteriores. +\end_layout + +\begin_layout Itemize + +\series bold +Prioridad: +\series default + De mayor a menor: +\begin_inset Formula $\neg$ +\end_inset + +, ( +\begin_inset Formula $\land$ +\end_inset + +, +\begin_inset Formula $\lor$ +\end_inset + +), ( +\begin_inset Formula $\rightarrow$ +\end_inset + +, +\begin_inset Formula $\leftrightarrow$ +\end_inset + +). +\end_layout + +\begin_layout Itemize + +\series bold +Asociatividad: +\series default + A igual prioridad de operadores, se asocia por la izquierda. +\end_layout + +\begin_layout Standard +También podemos añadir paréntesis a cualquier expresión que no sea una negación. +\end_layout + +\begin_layout Section +Formalización +\end_layout + +\begin_layout Itemize +Los átomos corresponden a oraciones enunciativas afirmativas, en forma presente + y con sujeto (salvo verbos impersonales). +\end_layout + +\begin_layout Itemize +\begin_inset Formula $\neg\alpha$ +\end_inset + +: No +\begin_inset Formula $\alpha$ +\end_inset + +, no es el caso de +\begin_inset Formula $\alpha$ +\end_inset + +, no es cierto que +\begin_inset Formula $\alpha$ +\end_inset + +, es falso que +\begin_inset Formula $\alpha$ +\end_inset + +, no sucede que +\begin_inset Formula $\alpha$ +\end_inset + +, la negación de +\begin_inset Formula $\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Itemize +\begin_inset Formula $\alpha\land\beta$ +\end_inset + +: +\begin_inset Formula $\alpha$ +\end_inset + + y +\begin_inset Formula $\beta$ +\end_inset + + (pero, aunque, además, sin embargo, también, a la vez, aún, no obstante). +\end_layout + +\begin_layout Itemize +\begin_inset Formula $\alpha\lor\beta$ +\end_inset + +: O +\begin_inset Formula $\alpha$ +\end_inset + + o +\begin_inset Formula $\beta$ +\end_inset + +; ya +\begin_inset Formula $\alpha$ +\end_inset + +, ya +\begin_inset Formula $\beta$ +\end_inset + +, ya ambas. +\end_layout + +\begin_layout Itemize +\begin_inset Formula $\alpha\rightarrow\beta$ +\end_inset + +: Si +\begin_inset Formula $\alpha$ +\end_inset + + +\begin_inset Formula $\beta$ +\end_inset + +, si +\begin_inset Formula $\alpha$ +\end_inset + + entonces +\begin_inset Formula $\beta$ +\end_inset + +, +\begin_inset Formula $\alpha$ +\end_inset + + solo si +\begin_inset Formula $\beta$ +\end_inset + +, solo +\begin_inset Formula $\alpha$ +\end_inset + + si +\begin_inset Formula $\beta$ +\end_inset + +, es suficiente +\begin_inset Formula $\alpha$ +\end_inset + + para que +\begin_inset Formula $\beta$ +\end_inset + +, siempre que +\begin_inset Formula $\alpha$ +\end_inset + + entonces +\begin_inset Formula $\beta$ +\end_inset + +, no +\begin_inset Formula $\alpha$ +\end_inset + + a menos que +\begin_inset Formula $\beta$ +\end_inset + +, es necesario +\begin_inset Formula $\beta$ +\end_inset + + para que +\begin_inset Formula $\alpha$ +\end_inset + +, a no ser que +\begin_inset Formula $\beta$ +\end_inset + + no +\begin_inset Formula $\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Itemize +\begin_inset Formula $\alpha\leftrightarrow\beta$ +\end_inset + +: +\begin_inset Formula $\alpha$ +\end_inset + + si y sólo si +\begin_inset Formula $\beta$ +\end_inset + +, +\begin_inset Formula $\alpha$ +\end_inset + + equivale a +\begin_inset Formula $\beta$ +\end_inset + +, +\begin_inset Formula $\alpha$ +\end_inset + + cuando y sólo cuando +\begin_inset Formula $\beta$ +\end_inset + +, +\begin_inset Formula $\alpha$ +\end_inset + + cuando únicamente +\begin_inset Formula $\beta$ +\end_inset + + , +\begin_inset Formula $\alpha$ +\end_inset + + es condición suficiente y necesaria para que +\begin_inset Formula $\beta$ +\end_inset + +. +\end_layout + +\begin_layout Section +Interpretación +\end_layout + +\begin_layout Standard +Procedimiento que traduce las fórmulas +\series bold +atómicas +\series default + a oraciones naturales. + Una +\series bold +asignación +\series default + +\begin_inset Formula $v_{I}$ +\end_inset + + es el procedimiento que establece un valor de verdad a una fórmula atómica + según una interpretación +\begin_inset Formula $I$ +\end_inset + +. + En L0 no se suele hacer distinción, y hace referencia a una función +\begin_inset Formula $v_{I}:{\cal P_{\alpha}}\rightarrow\mathbb{B}$ +\end_inset + + tal que +\begin_inset Formula $V\mapsto V$ +\end_inset + + y +\begin_inset Formula $F\mapsto F$ +\end_inset + +. +\end_layout + +\begin_layout Standard +La +\series bold +evaluación +\series default + es la obtención del valor de verdad de una oración +\begin_inset Formula $\alpha$ +\end_inset + +. + Decimos +\begin_inset Formula $V(\alpha)=V$ +\end_inset + + o +\begin_inset Formula $V(\alpha)=F$ +\end_inset + +, según corresponda. +\end_layout + +\begin_layout Itemize + +\series bold +Regla base: +\series default + Si +\begin_inset Formula $\alpha\in{\cal P}$ +\end_inset + +, entonces +\begin_inset Formula $V(\alpha)=v_{I}(\alpha)$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Regla recursiva: +\series default + +\begin_inset Formula +\begin{eqnarray*} +V(\neg\alpha) & = & \begin{cases} +V & \text{si }V(\alpha)=F\\ +F & \text{si }V(\alpha)=V +\end{cases}\\ +V(\alpha\land\beta) & = & \begin{cases} +V & \text{si }V(\alpha)=V\text{ y }V(\beta)=V\\ +F & \text{en otro caso} +\end{cases}\\ +V(\alpha\lor\beta) & = & \begin{cases} +F & \text{si }V(\alpha)=F\text{ y }V(\beta)=F\\ +V & \text{en otro caso} +\end{cases}\\ +V(\alpha\rightarrow\beta) & = & \begin{cases} +F & \text{si }V(\alpha)=V\text{ y }V(\beta)=F\\ +V & \text{en otro caso} +\end{cases}\\ +V(\alpha\leftrightarrow\beta) & = & \begin{cases} +V & \text{si }V(\alpha)=V(\beta)\\ +F & \text{en otro caso} +\end{cases} +\end{eqnarray*} + +\end_inset + + +\end_layout + +\begin_layout Section +Grafos semánticos +\end_layout + +\begin_layout Standard +Un grafo semántico es un árbol que representa una f.b.f. + El nodo principal contiene el operador principal (o el único átomo). + De cada conectivo parten dos ramas (o una si es +\begin_inset Formula $\neg$ +\end_inset + +) con las subfórmulas que conecta, y los átomos son hojas. +\end_layout + +\begin_layout Section +Decidibilidad +\end_layout + +\begin_layout Standard +Una oración puede ser: +\end_layout + +\begin_layout Itemize + +\series bold +Satisfacible +\series default + si +\begin_inset Formula $V(\alpha)=V$ +\end_inset + + en alguna interpretación. +\end_layout + +\begin_layout Itemize + +\series bold +Falseable +\series default + si +\begin_inset Formula $V(\alpha)=F$ +\end_inset + + en alguna interpretación. +\end_layout + +\begin_layout Itemize + +\series bold +Contingente +\series default + o +\series bold +contingencia +\series default + si es a la vez satisfacible y falseable. +\end_layout + +\begin_layout Itemize + +\series bold +Tautológica +\series default +, +\series bold +válida +\series default + o +\series bold +tautología +\series default + si +\begin_inset Formula $V(\alpha)=V$ +\end_inset + + en todas las interpretaciones. + Escribimos +\begin_inset Formula $\vDash\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Insatisfacible +\series default + o +\series bold +contradicción +\series default + si +\begin_inset Formula $V(\alpha)=F$ +\end_inset + + en todas las interpretaciones. +\end_layout + +\begin_layout Standard +El problema SAT, determinar si una oración lógica es satisfacible, es el + primer problema conocido NP-completo, y de hecho todos los problemas NP-complet +os se pueden reducir a SAT, de modo que si uno de resuelve como P, se resuelven + todos. +\end_layout + +\begin_layout Standard +Un conjunto de fórmulas +\begin_inset Formula ${\cal F}=\{\alpha_{1},\dots,\alpha_{n}\}$ +\end_inset + + es satisfacible si su conjunción lo es, y llamamos +\series bold +modelo +\series default + de +\begin_inset Formula ${\cal F}$ +\end_inset + + a cualquier interpretación en la que +\begin_inset Formula $V(\alpha_{1}\land\dots\land\alpha_{n})=V$ +\end_inset + +. + Definimos del mismo modo conjunto insatisfacible. + El conjunto +\begin_inset Formula ${\cal F}=\{\}$ +\end_inset + + es modelo en todas las interpretaciones. +\end_layout + +\begin_layout Standard +Para hallar los valores de verdad de una oración en función de la interpretación +, podemos construir una +\series bold +tabla de verdad. + +\series default + Si +\begin_inset Formula $\alpha$ +\end_inset + + tiene +\begin_inset Formula $n$ +\end_inset + + átomos y +\begin_inset Formula $m$ +\end_inset + + operadores, construimos una tabla con +\begin_inset Formula $2^{n}$ +\end_inset + + filas (más la cabecera) y +\begin_inset Formula $n+m$ +\end_inset + + columnas. + En cada fila establecemos una asignación hasta establecer todas las asignacione +s posibles y obtenemos las evaluaciones para las oraciones definidas por + cada operador, en orden de evaluación y terminando con el operador principal, + que establece el valor de verdad. + Debemos indicar el orden de evaluación. +\end_layout + +\begin_layout Standard +Otra forma es la +\series bold +propagación de literales. + +\series default + Un literal es un átomo o la negación de un átomo. + Dada una fórmula +\begin_inset Formula $\phi$ +\end_inset + +, definimos +\begin_inset Formula $\phi(p)\equiv\phi_{|V(p)=V}$ +\end_inset + + a la fórmula más simplificada que, en las interpretaciones en las que +\begin_inset Formula $V(p)=V$ +\end_inset + +, tenga los mismos valores de verdad que +\begin_inset Formula $\phi$ +\end_inset + +. + Por ejemplo, dada la oración +\begin_inset Formula $\phi\equiv(p\rightarrow q)\rightarrow(\neg p\rightarrow\neg q)$ +\end_inset + +, tendríamos que +\begin_inset Formula $\phi(p)\equiv\phi_{|V(p)=V}\equiv(V\rightarrow q)\rightarrow(\neg V\rightarrow\neg q)\equiv q\rightarrow(F\rightarrow q)\equiv q\rightarrow V\equiv V$ +\end_inset + +, mientras que +\begin_inset Formula $\phi(\neg p)\equiv\phi_{|V(\neg p)=V}\equiv\phi_{|V(p)=F}\equiv(F\rightarrow q)\rightarrow(\neg F\rightarrow\neg q)\equiv V\rightarrow(V\rightarrow\neg q)\equiv V\rightarrow\neg q\equiv\neg q$ +\end_inset + +. + En el segundo caso, tendríamos, por ejemplo, que +\begin_inset Formula $\phi(\neg p)(q)\equiv\phi(\neg p,q)\equiv\phi(\neg p)_{|V(q)=V}\equiv\neg V\equiv F$ +\end_inset + +. + En la práctica bastaría con escribir +\begin_inset Formula $\phi(\neg p,q)\equiv\neg V\equiv F$ +\end_inset + + para este último caso. +\end_layout + +\begin_layout Standard +Para comprobar los valores de verdad realizaríamos un +\series bold +árbol semántico. + +\series default + En este, la raíz sería la fórmula inicial, y de cada nodo, que contendrá + una fórmula +\begin_inset Formula $\xi$ +\end_inset + +, partirán dos ramas con +\begin_inset Formula $\xi(p)$ +\end_inset + + y +\begin_inset Formula $\xi(\neg p)$ +\end_inset + + para algún átomo +\begin_inset Formula $l$ +\end_inset + + en +\begin_inset Formula $\xi$ +\end_inset + + (normalmente el que más aparece), salvo si +\begin_inset Formula $\xi\equiv V$ +\end_inset + + o +\begin_inset Formula $\xi\equiv F$ +\end_inset + +. + A la hora de dibujarlo, la línea que une una expresión con otra derivada + se etiqueta con el literal a propagar. +\end_layout + +\begin_layout Section +Equivalencias +\end_layout + +\begin_layout Standard +Dos expresiones +\begin_inset Formula $\alpha$ +\end_inset + + y +\begin_inset Formula $\beta$ +\end_inset + + son lógicamente equivalentes si y sólo si +\begin_inset Formula $V(\alpha)=V(\beta)$ +\end_inset + + para cualquier interpretación. + Escribimos +\begin_inset Formula $\alpha\equiv\beta$ +\end_inset + +. + Así, +\begin_inset Formula $\alpha\equiv\beta\iff\vDash\alpha\leftrightarrow\beta$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Propiedades conmutativas: +\series default + +\begin_inset Formula $\alpha\land\beta\equiv\beta\land\alpha$ +\end_inset + +; +\begin_inset Formula $\alpha\lor\beta\equiv\beta\land\alpha$ +\end_inset + +; +\begin_inset Formula $\alpha\leftrightarrow\beta\equiv\beta\leftrightarrow\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Propiedades asociativas: +\series default + +\begin_inset Formula $\alpha\land(\beta\land\gamma)\equiv(\alpha\land\beta)\land\gamma$ +\end_inset + +; +\begin_inset Formula $\alpha\lor(\beta\lor\gamma)\equiv(\alpha\lor\beta)\lor\gamma$ +\end_inset + +; +\begin_inset Formula $\alpha\leftrightarrow(\beta\leftrightarrow\gamma)\equiv(\alpha\leftrightarrow\beta)\leftrightarrow\gamma$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Propiedades de De Morgan: +\series default + +\begin_inset Formula $\neg(\alpha\land\beta)\equiv\neg\alpha\lor\neg\beta$ +\end_inset + +; +\begin_inset Formula $\neg(\alpha\lor\beta)\equiv\neg\alpha\land\neg\beta$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Propiedades distributivas: +\series default + +\begin_inset Formula $\alpha\land(\beta\lor\gamma)\equiv(\alpha\land\beta)\lor(\alpha\land\gamma)$ +\end_inset + +; +\begin_inset Formula $\alpha\lor(\beta\land\gamma)\equiv(\alpha\lor\beta)\land(\alpha\lor\gamma)$ +\end_inset + +; +\begin_inset Formula $\alpha\rightarrow(\beta\lor\gamma)\equiv(\alpha\rightarrow\beta)\lor(\alpha\rightarrow\gamma)$ +\end_inset + +; +\begin_inset Formula $\alpha\rightarrow(\beta\land\gamma)\equiv(\alpha\rightarrow\beta)\land(\alpha\rightarrow\gamma)$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Propiedades de absorción: +\series default + +\begin_inset Formula $\alpha\lor(\alpha\land\beta)\equiv\alpha\land(\alpha\lor\beta)\equiv\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Expresión booleana: +\series default + +\begin_inset Formula $\alpha\lor(\neg\beta\land\beta)\equiv\alpha\land(\neg\beta\lor\beta)\equiv\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Reducción al absurdo: +\series default + +\begin_inset Formula $\neg\alpha\rightarrow(\beta\land\neg\beta)\equiv\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Propiedad de contraposición +\series default + o +\series bold +transposición: +\series default + +\begin_inset Formula $\alpha\rightarrow\beta\equiv\neg\beta\rightarrow\neg\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Exportación: +\series default + +\begin_inset Formula $(\alpha\land\beta)\rightarrow\gamma\equiv\alpha\rightarrow(\beta\rightarrow\gamma)$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Idempotencia: +\series default + +\begin_inset Formula $\alpha\equiv\neg(\neg\alpha)\equiv\alpha\lor\alpha\equiv\alpha\land\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Eliminación del condicional: +\series default + +\begin_inset Formula $\alpha\rightarrow\beta\equiv\neg\alpha\lor\beta\equiv\neg(\alpha\land\neg\beta)$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Eliminación del bicondicional: +\series default + +\begin_inset Formula $\alpha\leftrightarrow\beta\equiv(\alpha\rightarrow\beta)\land(\beta\rightarrow\alpha)\equiv(\alpha\land\beta)\lor(\neg\beta\land\neg\alpha)$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Propiedades sobre tautologías: +\series default + +\begin_inset Formula $\alpha\lor\neg\alpha\equiv V$ +\end_inset + +; +\begin_inset Formula $V\lor\beta\equiv V$ +\end_inset + +; +\begin_inset Formula $V\land\beta\equiv\beta$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Propiedades sobre insatisfacibilidad: +\series default + +\begin_inset Formula $\alpha\land\neg\alpha\equiv F$ +\end_inset + +; +\begin_inset Formula $F\lor\beta\equiv\beta$ +\end_inset + +; +\begin_inset Formula $F\land\beta\equiv F$ +\end_inset + +. +\end_layout + +\begin_layout Section +Razonamientos válidos +\end_layout + +\begin_layout Standard +Un razonamiento es válido si y sólo si en todas las interpretaciones en + las que +\begin_inset Formula $\alpha$ +\end_inset + + es verdad, +\begin_inset Formula $\beta$ +\end_inset + + también lo es. + Igualmente, +\begin_inset Formula $\beta$ +\end_inset + + es +\series bold +consecuencia lógica +\series default + de +\begin_inset Formula ${\cal F}=\{\alpha_{1},\dots,\alpha_{n}\}$ +\end_inset + + si +\begin_inset Formula $\beta$ +\end_inset + + es verdad siempre que +\begin_inset Formula ${\cal F}$ +\end_inset + + sea un modelo. + Escribimos +\begin_inset Formula $\alpha\vDash\beta$ +\end_inset + + o +\begin_inset Formula ${\cal F}\vDash\beta$ +\end_inset + +, y sabemos que +\begin_inset Formula $\alpha\vDash\beta\iff\vDash\alpha\rightarrow\beta$ +\end_inset + +. +\end_layout + +\begin_layout Standard + +\series bold +Teorema de la deducción semántica: +\series default + +\begin_inset Formula ${\cal F}\cup\{\alpha\}\vDash\beta\iff{\cal F}\vDash\alpha\rightarrow\beta$ +\end_inset + +. + Corolario: +\begin_inset Formula ${\cal F}\vDash\beta\iff\vDash\alpha_{1}\land\dots\land\alpha_{n}\rightarrow\beta\iff\vDash\neg(\alpha_{1}\land\dots\land\alpha_{n}\land\neg\beta)\iff\alpha_{1}\land\dots\land\alpha_{n}\land\neg\beta\text{ es insatisfacible}$ +\end_inset + +. + Propiedades generales de +\begin_inset Formula $\vDash$ +\end_inset + +: +\end_layout + +\begin_layout Itemize + +\series bold +Reflexividad: +\series default + +\begin_inset Formula $\alpha\vDash\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Transitividad: +\series default + Si +\begin_inset Formula ${\cal F}\vDash\alpha$ +\end_inset + + y +\begin_inset Formula $\alpha\vDash\beta$ +\end_inset + + entonces +\begin_inset Formula ${\cal F}\vDash\beta$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Monotonía: +\series default + Si +\begin_inset Formula ${\cal F}\vDash\alpha$ +\end_inset + + entonces +\begin_inset Formula ${\cal F}\cup\{\beta\}\vDash\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Itemize +Si +\begin_inset Formula ${\cal F}\vDash\alpha$ +\end_inset + + y +\begin_inset Formula $\vDash\beta$ +\end_inset + +, entonces +\begin_inset Formula ${\cal F}\backslash\{\beta\}\vDash\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Itemize +\begin_inset Formula $\alpha\equiv\beta\iff\alpha\vDash\beta\text{ y }\beta\vDash\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Standard +Algunas propiedades: +\end_layout + +\begin_layout Itemize + +\series bold +Simplificación +\series default + o +\series bold +eliminación de la conjunción: +\series default + +\begin_inset Formula $\alpha\land\beta\vDash\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Adición +\series default + o +\series bold +introducción de la disyunción: +\series default + +\begin_inset Formula $\alpha\vDash\alpha\lor\beta$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Silogismos: +\series default + Forma de razonamiento deductivo con dos premisas y una conclusión. +\end_layout + +\begin_deeper +\begin_layout Itemize + +\series bold +Categóricos +\end_layout + +\begin_deeper +\begin_layout Itemize + +\series bold +Combinación +\series default + o +\series bold +introducción de la conjunción: +\series default + +\begin_inset Formula $\{\alpha,\beta\}\vDash\alpha\land\beta$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Inconsistencia: +\series default + +\begin_inset Formula $\{\alpha,\neg\alpha\}\vDash\beta$ +\end_inset + +. +\end_layout + +\end_deeper +\begin_layout Itemize + +\series bold +Hipotéticos +\end_layout + +\begin_deeper +\begin_layout Itemize + +\series bold +Silogismo hipotético: +\series default + +\begin_inset Formula $\{\alpha\rightarrow\beta,\beta\rightarrow\gamma\}\vDash\alpha\rightarrow\gamma$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Demostración por casos: +\series default + +\begin_inset Formula $\{\alpha\rightarrow\gamma,\beta\rightarrow\gamma\}\vDash\alpha\lor\beta\rightarrow\gamma$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Prueba por casos: +\series default + +\begin_inset Formula $\{\alpha\rightarrow\beta,\neg\alpha\rightarrow\beta\}\vDash\beta$ +\end_inset + +. +\end_layout + +\end_deeper +\begin_layout Itemize + +\series bold +Hipotéticos mixtos +\end_layout + +\begin_deeper +\begin_layout Itemize + +\series bold +Modus Ponens: +\series default + +\begin_inset Formula $\{\alpha\rightarrow\beta,\alpha\}\vDash\beta$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Modus Tollens: +\series default + +\begin_inset Formula $\{\alpha\rightarrow\beta,\neg\beta\}\vDash\neg\alpha$ +\end_inset + +. +\end_layout + +\end_deeper +\begin_layout Itemize + +\series bold +Disyuntivo: +\series default + +\begin_inset Formula $\{\alpha\lor\beta,\neg\beta\}\vDash\alpha$ +\end_inset + +. +\end_layout + +\end_deeper +\begin_layout Itemize + +\series bold +Dilemas: +\series default + Forma de razonamiento con una premisa disyunción que representa las opciones, + normalmente contrarias. +\end_layout + +\begin_deeper +\begin_layout Itemize + +\series bold +Constructivo: +\series default + +\begin_inset Formula $\{\alpha\lor\beta,\alpha\rightarrow\gamma,\beta\rightarrow\delta\}\vDash\gamma\lor\delta$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Destructivo: +\series default + +\begin_inset Formula $\{\neg\gamma\lor\neg\delta,\alpha\rightarrow\gamma,\beta\rightarrow\delta\}\vDash\neg\alpha\lor\neg\beta$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Transposición: +\series default + +\begin_inset Formula $\alpha\rightarrow\beta\vDash\neg\beta\rightarrow\neg\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Eliminación de la equivalencia: +\series default + +\begin_inset Formula $\alpha\leftrightarrow\beta\vDash\{\alpha\rightarrow\beta,\beta\rightarrow\alpha\}$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Introducción de la equivalencia: +\series default + +\begin_inset Formula $\{\alpha\rightarrow\beta,\beta\rightarrow\alpha\}\vDash\alpha\leftrightarrow\beta$ +\end_inset + +. +\end_layout + +\end_deeper +\begin_layout Standard +El Corolario del Teorema de la Deducción Semántica y las propiedades básicas + de equivalencia y razonamientos nos permiten considerar al menos dos estrategia +s de razonamiento deductivo: la +\series bold +demostración directa +\series default +, comprobando que +\begin_inset Formula $\beta$ +\end_inset + + es consecuencia lógica de +\begin_inset Formula $\alpha$ +\end_inset + + mediante definiciones, tautologías, teoremas o propiedades, y +\series bold +refutación +\series default + o demostración por contradicción ( +\begin_inset Formula $\alpha\rightarrow\beta\equiv\alpha\land\neg\beta\implies\gamma\land\neg\gamma$ +\end_inset + +), buscando contraejemplos o encontrando un +\begin_inset Formula $a$ +\end_inset + + tal que +\begin_inset Formula $V(\alpha[a]\rightarrow\beta[a])=F$ +\end_inset + +. +\end_layout + +\end_body +\end_document diff --git a/fli/n3.lyx b/fli/n3.lyx new file mode 100644 index 0000000..f720c27 --- /dev/null +++ b/fli/n3.lyx @@ -0,0 +1,1512 @@ +#LyX 2.3 created this file. For more info see http://www.lyx.org/ +\lyxformat 544 +\begin_document +\begin_header +\save_transient_properties true +\origin unavailable +\textclass book +\use_default_options true +\maintain_unincluded_children false +\language spanish +\language_package default +\inputencoding auto +\fontencoding global +\font_roman "default" "default" +\font_sans "default" "default" +\font_typewriter "default" "default" +\font_math "auto" "auto" +\font_default_family default +\use_non_tex_fonts false +\font_sc false +\font_osf false +\font_sf_scale 100 100 +\font_tt_scale 100 100 +\use_microtype false +\use_dash_ligatures true +\graphics default +\default_output_format default +\output_sync 0 +\bibtex_command default +\index_command default +\paperfontsize default +\spacing single +\use_hyperref false +\papersize default +\use_geometry false +\use_package amsmath 1 +\use_package amssymb 1 +\use_package cancel 1 +\use_package esint 1 +\use_package mathdots 1 +\use_package mathtools 1 +\use_package mhchem 1 +\use_package stackrel 1 +\use_package stmaryrd 1 +\use_package undertilde 1 +\cite_engine basic +\cite_engine_type default +\biblio_style plain +\use_bibtopic false +\use_indices false +\paperorientation portrait +\suppress_date false +\justification true +\use_refstyle 1 +\use_minted 0 +\index Index +\shortcut idx +\color #008000 +\end_index +\secnumdepth 3 +\tocdepth 3 +\paragraph_separation indent +\paragraph_indentation default +\is_math_indent 0 +\math_numbering_side default +\quotes_style swiss +\dynamic_quotes 0 +\papercolumns 1 +\papersides 1 +\paperpagestyle default +\tracking_changes false +\output_changes false +\html_math_output 0 +\html_css_as_file 0 +\html_be_strict false +\end_header + +\begin_body + +\begin_layout Section +Algoritmos que no requieren cláusulas +\end_layout + +\begin_layout Subsection +Tablas de verdad +\end_layout + +\begin_layout Standard +Construimos una tabla de verdad por filas, y si en una fila obtenemos que + la oración es cierta para dicha interpretación, la oración es satisfacible. + Si no es cierta en ninguna, la oración es insatisfacible. +\end_layout + +\begin_layout Subsection +Árboles semánticos +\end_layout + +\begin_layout Standard +Una hoja de un árbol semántico es un +\series bold +nodo fallo +\series default + si su etiqueta es +\begin_inset Formula $F$ +\end_inset + +, y +\series bold +nodo éxito +\series default + si es +\begin_inset Formula $V$ +\end_inset + +. + Representamos el árbol como +\begin_inset Formula $\vernal$ +\end_inset + +, y observamos que, para comprobar la satisfacibilidad, basta con encontrar + un nodo éxito, y entonces no es necesario seguir desarrollando. +\end_layout + +\begin_layout Subsection +Tableaux semánticos +\end_layout + +\begin_layout Standard +Un +\series bold +tableaux semántico +\series default + es un árbol en el cual cada nodo está formado por una lista de oraciones + (sin paréntesis de ningún tipo), y su raíz es la lista formada por la oración + +\begin_inset Formula $\phi$ +\end_inset + + a desarrollar. + Una oración puede tener +\series bold +comportamiento conjuntivo +\series default + (se le puede aplicar una +\begin_inset Formula $\alpha$ +\end_inset + +-fórmula) o +\series bold +disyuntivo +\series default + (se le puede aplicar una +\begin_inset Formula $\beta$ +\end_inset + +-fórmula), o ser un literal. + Para cada rama del árbol: +\end_layout + +\begin_layout Enumerate +Seleccionamos una oración que no sea un literal, preferiblemente con comportamie +nto conjuntivo. +\end_layout + +\begin_layout Enumerate +Si no encontramos ninguna, el nodo es un nodo hoja. + Lo marcamos como +\series bold +cerrado +\series default + si contiene un literal y su contrario, de lo contrario como +\series bold +abierto +\series default +. +\end_layout + +\begin_layout Enumerate +Si tiene comportamiento conjuntivo, aplicamos la +\begin_inset Formula $\alpha$ +\end_inset + +-fórmula correspondiente y dibujamos una rama con la etiqueta +\begin_inset Formula $\alpha:\text{(nom. de fórmula)}$ +\end_inset + + y el nodo resultado de sustituir +\begin_inset Formula $\alpha,\phi_{1},\dots,\phi_{n}$ +\end_inset + + por +\begin_inset Formula $\alpha_{1},\alpha_{2},\phi_{1},\dots,\phi_{n}$ +\end_inset + +. +\end_layout + +\begin_layout Enumerate +Si tiene comportamiento disyuntivo, aplicamos la +\begin_inset Formula $\beta$ +\end_inset + +-fórmula correspondiente y dibujamos dos ramas. + La división se marca con la etiqueta +\begin_inset Formula $\beta:\text{(nom. de fórmula)}$ +\end_inset + + y los nodos son los resultantes de sustituir +\begin_inset Formula $\beta,\phi_{1},\dots,\phi_{n}$ +\end_inset + + por +\begin_inset Formula $\beta_{1},\phi_{1},\dots,\phi_{n}$ +\end_inset + + y +\begin_inset Formula $\beta_{2},\phi_{1},\dots,\phi_{n}$ +\end_inset + +. +\end_layout + +\begin_layout Standard +\align center +\begin_inset Tabular + + + + + + + + + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha$ +\end_inset + +-fórmulas +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\beta$ +\end_inset + +-fórmulas +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset + + + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha_{1}$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha_{2}$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\beta$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\beta_{1}$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\beta_{2}$ +\end_inset + + +\end_layout + +\end_inset + + + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg\neg\alpha$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset + + + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha\land\beta$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\beta$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg(\alpha\land\beta)$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg\alpha$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg\beta$ +\end_inset + + +\end_layout + +\end_inset + + + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg(\alpha\lor\beta)$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg\alpha$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg\beta$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha\lor\beta$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\beta$ +\end_inset + + +\end_layout + +\end_inset + + + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg(\alpha\rightarrow\beta)$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg\beta$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha\rightarrow\beta$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg\alpha$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\beta$ +\end_inset + + +\end_layout + +\end_inset + + + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha\leftrightarrow\beta$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha\rightarrow\beta$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\beta\rightarrow\alpha$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg(\alpha\leftrightarrow\beta)$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg(\alpha\rightarrow\beta)$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg(\beta\rightarrow\alpha)$ +\end_inset + + +\end_layout + +\end_inset + + + + +\end_inset + + +\end_layout + +\begin_layout Standard +Un +\series bold +tableaux completado +\series default + o +\series bold +completo +\series default + es aquel cuya construcción ha terminado. + Decimos que es +\series bold +cerrado +\series default + cuando todas las hojas son cerradas, y +\series bold +abierto +\series default + cuando hay alguna abierta. + Así, +\begin_inset Formula $\phi$ +\end_inset + + es satisfacible si y sólo si su tableau completado es abierto. + Este método no detecta tautologías, pero podemos determinar que +\begin_inset Formula $\phi$ +\end_inset + + es tautológica cuando +\begin_inset Formula $\neg\phi$ +\end_inset + + es insatisfacible. +\end_layout + +\begin_layout Section +Algoritmos que requieren cláusulas +\end_layout + +\begin_layout Standard +Una fórmula +\begin_inset Formula $\xi$ +\end_inset + + está en +\series bold +forma normal conjuntiva +\series default + si es una cláusula o conjunción de cláusulas. + Una +\series bold +cláusula +\series default + es un literal o disyunción de dos o más literales (quitando todos los paréntesi +s). +\end_layout + +\begin_layout Itemize + +\series bold +Cláusula unitaria: +\series default + Con un solo literal. +\end_layout + +\begin_layout Itemize + +\series bold +Cláusula vacía: +\series default + Sin literales. + Se denota por +\begin_inset Formula $\square$ +\end_inset + + y es insatisfacible. +\end_layout + +\begin_layout Itemize + +\series bold +Cláusula de Horn: +\series default + Aquella que tiene como máximo un literal positivo. +\end_layout + +\begin_layout Standard +Llamamos +\series bold +conjunto clausal +\series default + o +\series bold +clausulado +\series default + al conjunto de dichas cláusulas, y decimos que está en +\series bold +forma clausal +\series default +. +\end_layout + +\begin_layout Subsection +Obtención de FNC +\end_layout + +\begin_layout Enumerate +Aplicar las reglas de eliminación de +\begin_inset Formula $\leftrightarrow$ +\end_inset + + y +\begin_inset Formula $\rightarrow$ +\end_inset + + hasta tener solo +\begin_inset Formula $\neg$ +\end_inset + +, +\begin_inset Formula $\land$ +\end_inset + + y +\begin_inset Formula $\lor$ +\end_inset + +. +\end_layout + +\begin_layout Enumerate +Aplicar De Morgan hasta que las negaciones solo afecten a átomos. +\end_layout + +\begin_layout Enumerate +Eliminar las negaciones múltiples ( +\begin_inset Formula $\neg\neg$ +\end_inset + +). +\end_layout + +\begin_layout Enumerate +Aplicar distributividad de +\begin_inset Formula $\lor$ +\end_inset + + sobre +\begin_inset Formula $\land$ +\end_inset + +. +\end_layout + +\begin_layout Enumerate +Reducir la cantidad de paréntesis. +\end_layout + +\begin_layout Standard +Si queremos simplificar: +\end_layout + +\begin_layout Enumerate +Eliminar literales opuestos: +\begin_inset Formula $\ell\lor\neg\ell\equiv V$ +\end_inset + +; +\begin_inset Formula $\ell\land\neg\ell\equiv F$ +\end_inset + +. +\end_layout + +\begin_layout Enumerate +Eliminar constantes y expresiones repetidas: +\begin_inset Formula $V\lor\alpha\equiv V$ +\end_inset + +; +\begin_inset Formula $F\lor\alpha\equiv V\land\alpha\equiv\alpha$ +\end_inset + +; +\begin_inset Formula $F\land\alpha\equiv F$ +\end_inset + +; +\begin_inset Formula $\alpha\lor\alpha\equiv\alpha\land\alpha\equiv\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Enumerate +Quedarnos con expresiones subsumidas: +\begin_inset Formula $(\alpha\lor\beta)\land\alpha\equiv\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Subsection +Algoritmo DPLL +\end_layout + +\begin_layout Standard +Al propagar un literal en una expresión en FNC, lo que hacemos es eliminar + las cláusulas en las que aparezca ( +\series bold +cláusula cancelada +\series default +) y las ocurrencias de literales complementarios ( +\series bold +ocurrencia eliminada +\series default +). + Al aplicar DPLL, representamos el conjunto clausulado como un conjunto + de conjuntos. + Por ejemplo, si +\begin_inset Formula $\phi\equiv p\land(q\lor\neg r)$ +\end_inset + +, entonces su conjunto clausal es +\begin_inset Formula $\Omega_{\phi}=\{p,q\lor\neg r\}$ +\end_inset + +, y lo representamos como +\begin_inset Formula $\Omega_{\phi FNC}=\{p,\{q,\neg r\}\}$ +\end_inset + +. + Entonces consideramos 5 reglas: +\end_layout + +\begin_layout Enumerate + +\series bold +Regla de la cláusula unitaria: +\series default + Si hay una cláusula unitaria, propagar su literal. +\end_layout + +\begin_layout Enumerate + +\series bold +Regla del literal puro: +\series default + Si hay un literal para el que no se da su complementario, propagarlo. +\end_layout + +\begin_layout Enumerate + +\series bold +Regla de la tautología: +\series default + Eliminar las cláusulas que contengan literales complementarios. +\end_layout + +\begin_layout Enumerate + +\series bold +Regla de la inclusión: +\series default + Si existen conjuntos clausales +\begin_inset Formula $C_{1},C_{2}\in\Omega_{\phi}$ +\end_inset + + tales que +\begin_inset Formula $C_{1}\subseteq C_{2}$ +\end_inset + +, eliminar +\begin_inset Formula $C_{2}$ +\end_inset + + de +\begin_inset Formula $\Omega_{\phi}$ +\end_inset + +. +\end_layout + +\begin_layout Enumerate + +\series bold +Regla de ramificación: +\series default + Considerar un literal +\begin_inset Formula $l$ +\end_inset + + (normalmente el que aparece más veces) y propagar +\begin_inset Formula $l$ +\end_inset + + por un lado y +\begin_inset Formula $\neg l$ +\end_inset + + por otro. +\end_layout + +\begin_layout Standard +El algoritmo consiste en: +\end_layout + +\begin_layout Enumerate +Si +\begin_inset Formula $\Omega_{\phi}=\{\}$ +\end_inset + +, devolver +\family typewriter +true +\family default + (se indica mediante una flecha de la expresión derivada a la original etiquetad +a +\begin_inset Quotes cld +\end_inset + +true +\begin_inset Quotes crd +\end_inset + +), indicando que es satisfacible. +\end_layout + +\begin_layout Enumerate +Si +\begin_inset Formula $\square\in\Omega_{\phi}$ +\end_inset + +, devolver +\family typewriter +false +\family default +. +\end_layout + +\begin_layout Enumerate +En caso contrario, aplicar la primera de las reglas que sea aplicable y + devolver su va +\begin_inset ERT +status open + +\begin_layout Plain Layout + + +\backslash +- +\end_layout + +\end_inset + +lor. + Para la regla de ramificación: Si la primera rama devuelve +\family typewriter +true +\family default +, devolverlo. + Si no, proceder con la segunda rama y devolver el valor devuelto. + Esto es lo que se denomina +\begin_inset Quotes cld +\end_inset + + +\lang american +backtracking +\lang spanish + +\begin_inset Quotes crd +\end_inset + + (a partir de un algoritmo recursivo). +\end_layout + +\begin_layout Standard +Lo representamos con un grafo, similar al del árbol semántico. +\end_layout + +\begin_layout Subsection +Método de resolución +\end_layout + +\begin_layout Standard +La +\series bold +resolvente +\series default + de dos cláusulas +\begin_inset Formula $\psi\equiv l_{1}\lor\dots\lor l_{n}\lor j$ +\end_inset + + y +\begin_inset Formula $\text{\phi}\equiv k_{1}\lor\dots\lor k_{m}\lor\neg j$ +\end_inset + + es la cláusula +\begin_inset Formula $R_{j}(\psi,\phi)\equiv l_{1}\lor\dots\lor l_{n}\lor k_{1}\lor\dots\lor k_{m}$ +\end_inset + +. + +\begin_inset Formula $\psi$ +\end_inset + + y +\begin_inset Formula $\phi$ +\end_inset + + son las +\series bold +cláusulas padres +\series default + de +\begin_inset Formula $R_{j}(\psi,\phi)$ +\end_inset + +, y +\begin_inset Formula $\{\psi,\phi\}$ +\end_inset + + es satisfacible si y sólo si +\begin_inset Formula $R_{j}(\psi,\phi)$ +\end_inset + + lo es. + Para resolver por resolución: +\end_layout + +\begin_layout Enumerate +Definimos el conjunto +\begin_inset Formula ${\cal C}=\Omega_{\phi}$ +\end_inset + + y +\begin_inset Formula ${\cal C}_{0}^{*}={\cal C}$ +\end_inset + +. +\end_layout + +\begin_layout Enumerate +Por cada par de cláusulas +\begin_inset Formula $C_{1}=l\lor\alpha$ +\end_inset + + y +\begin_inset Formula $C_{2}=\neg l\lor\beta$ +\end_inset + + en +\begin_inset Formula ${\cal C}^{*}$ +\end_inset + +, obtenemos su resolvente y la añadimos a +\begin_inset Formula ${\cal C}^{*}$ +\end_inset + +. + Si obtenemos la resolvente +\begin_inset Formula $\square$ +\end_inset + +, el conjunto +\begin_inset Formula ${\cal C}^{*}$ +\end_inset + + es insatisfacible y por tanto +\begin_inset Formula ${\cal C}$ +\end_inset + + también. +\end_layout + +\begin_layout Enumerate +Una vez obtenidas todas las resolventes, si +\begin_inset Formula $\square\notin{\cal C}^{*}$ +\end_inset + +, entonces +\begin_inset Formula ${\cal C}^{*}$ +\end_inset + + es satisfacible y por tanto +\begin_inset Formula ${\cal C}$ +\end_inset + + también (solo en L0). +\end_layout + +\begin_layout Standard +Podemos expresar este algoritmo mediante un +\series bold +grafo de resolución +\series default +, en el que de cada par de cláusulas posible parte una línea hacia abajo + hacia su resolvente y tenemos cuidado de no incluir un resolvente igual + a una cláusula ya existente. +\end_layout + +\begin_layout Standard +En dicho grafo, las premisas se dice que están en el nivel 0 ( +\begin_inset Formula ${\cal C}$ +\end_inset + +), y si +\begin_inset Formula $C_{1}$ +\end_inset + + y +\begin_inset Formula $C_{2}$ +\end_inset + + están en los niveles +\begin_inset Formula $x_{1}$ +\end_inset + + y +\begin_inset Formula $x_{2}$ +\end_inset + +, su resolvente está en el nivel +\begin_inset Formula $\max\{x_{1},x_{2}\}+1$ +\end_inset + +, de forma que cada nivel se representa en una misma línea horizontal, y + los resolventes se numeran empezando por el nivel más alto (el nivel 0). +\end_layout + +\begin_layout Standard +Un grafo de resolución es +\series bold +básico +\series default + si solo muestra dos cláusulas y su resolvente; +\series bold +completo +\series default + si contiene la unión de todos los grafos de resolución básicos, y es un + +\series bold +grafo de refutación +\series default + si aparece +\begin_inset Formula $\square$ +\end_inset + +. +\end_layout + +\begin_layout Standard +Para la elección de los pares de cláusulas padres, existen principalmente + dos +\series bold +estrategias de resolución: +\end_layout + +\begin_layout Itemize + +\series bold +Búsqueda en anchura: +\series default + Se obtienen todas las resolventes de un nivel antes de pasar al siguiente. + Orden +\begin_inset Formula $(2,1)$ +\end_inset + +, +\begin_inset Formula $(3,1)$ +\end_inset + +, +\begin_inset Formula $(3,2)$ +\end_inset + +, +\begin_inset Formula $(4,1)$ +\end_inset + +, etc. +\end_layout + +\begin_layout Itemize + +\series bold +Búsqueda en profundidad: +\series default + Una vez obtenida una resolvente de nivel +\begin_inset Formula $i$ +\end_inset + +, intenta obtener una de nivel +\begin_inset Formula $i+1$ +\end_inset + + a partir de ella. + Orden +\begin_inset Formula $(2,1)\rightarrow i$ +\end_inset + +, +\begin_inset Formula $(i,1)$ +\end_inset + +, +\begin_inset Formula $(i,2)$ +\end_inset + +, +\begin_inset Formula $(i,3)\rightarrow j$ +\end_inset + +, +\begin_inset Formula $(j,1)$ +\end_inset + +, etc. + No es completa. +\end_layout + +\begin_layout Standard +En la práctica se utiliza la +\series bold +notación +\series default + o +\series bold +representación Fitting +\series default +: Se crea una lista numerada de las cláusulas de +\begin_inset Formula ${\cal C}$ +\end_inset + +, con la indicación +\begin_inset Quotes cld +\end_inset + +Premisa +\begin_inset Quotes crd +\end_inset + + o +\begin_inset Quotes cld +\end_inset + +C.E. +\begin_inset Quotes crd +\end_inset + + (conjunto de entrada) a la derecha de cada una. + Después, se van comprobando los pares de cláusulas en la lista, empezando + por +\begin_inset Formula $(2,1)$ +\end_inset + +, +\begin_inset Formula $(3,1)$ +\end_inset + +, +\begin_inset Formula $(3,2)$ +\end_inset + +, etc., y se va ampliando con los resolventes, que tendrán la indicación + +\begin_inset Formula $R_{l}(i,j)$ +\end_inset + +, siendo +\begin_inset Formula $i$ +\end_inset + + y +\begin_inset Formula $j$ +\end_inset + + los ordinales de las cláusulas padres. + Para optimizar, se pueden tachar cláusulas por los siguientes motivos: +\end_layout + +\begin_layout Itemize +Literal puro ( +\begin_inset Formula $l$ +\end_inset + +) [después de tachar ( +\begin_inset Formula $n$ +\end_inset + +)]. +\end_layout + +\begin_layout Itemize +Subsumida en ( +\begin_inset Formula $n$ +\end_inset + +). +\end_layout + +\begin_layout Itemize +Tautología ( +\begin_inset Formula $l\lor\neg l$ +\end_inset + +). +\end_layout + +\begin_layout Standard +El motivo debe indicarse a la derecha. + Si al final queda +\begin_inset Formula ${\cal C}^{*}=\{\}$ +\end_inset + +, la oración es satisfacible. +\end_layout + +\begin_layout Section +Razonamiento automático +\end_layout + +\begin_layout Standard +Un razonamiento es válido ( +\begin_inset Formula $\{\alpha_{1},\dots,\alpha_{n}\}\vDash\beta$ +\end_inset + +) cuando +\begin_inset Formula $\vDash\alpha_{1}\land\dots\land\alpha_{n}\rightarrow\beta$ +\end_inset + +, es decir, cuando +\begin_inset Formula $\alpha_{1}\land\dots\land\alpha_{n}\land\neg\beta$ +\end_inset + + es insatisfacible. + Así, mediante tablas de verdad o árboles semánticos, podemos determinar + la validez de un razonamiento demostrando que +\begin_inset Formula $\alpha_{1}\land\dots\land\alpha_{n}\rightarrow\beta$ +\end_inset + + es una tautología. + Para el resto de los métodos, comprobamos que +\begin_inset Formula $\alpha_{1}\land\dots\land\alpha_{n}\land\neg\beta$ +\end_inset + + es una contradicción. +\end_layout + +\begin_layout Standard +En el caso de demostración por resolución, las cláusulas de +\begin_inset Formula $\neg\beta$ +\end_inset + + se denominan +\begin_inset Quotes cld +\end_inset + +conjunto soporte de entrada +\begin_inset Quotes crd +\end_inset + +. + Se marcan con un +\begin_inset Formula $*$ +\end_inset + + a la izquierda del ordinal tanto estas como las resolventes de alguna cláusula + marcada con +\begin_inset Formula $*$ +\end_inset + +, de forma recursiva. +\end_layout + +\end_body +\end_document diff --git a/fli/n4.lyx b/fli/n4.lyx new file mode 100644 index 0000000..3796419 --- /dev/null +++ b/fli/n4.lyx @@ -0,0 +1,402 @@ +#LyX 2.3 created this file. For more info see http://www.lyx.org/ +\lyxformat 544 +\begin_document +\begin_header +\save_transient_properties true +\origin unavailable +\textclass book +\use_default_options true +\maintain_unincluded_children false +\language spanish +\language_package default +\inputencoding auto +\fontencoding global +\font_roman "default" "default" +\font_sans "default" "default" +\font_typewriter "default" "default" +\font_math "auto" "auto" +\font_default_family default +\use_non_tex_fonts false +\font_sc false +\font_osf false +\font_sf_scale 100 100 +\font_tt_scale 100 100 +\use_microtype false +\use_dash_ligatures true +\graphics default +\default_output_format default +\output_sync 0 +\bibtex_command default +\index_command default +\paperfontsize default +\spacing single +\use_hyperref false +\papersize default +\use_geometry false +\use_package amsmath 1 +\use_package amssymb 1 +\use_package cancel 1 +\use_package esint 1 +\use_package mathdots 1 +\use_package mathtools 1 +\use_package mhchem 1 +\use_package stackrel 1 +\use_package stmaryrd 1 +\use_package undertilde 1 +\cite_engine basic +\cite_engine_type default +\biblio_style plain +\use_bibtopic false +\use_indices false +\paperorientation portrait +\suppress_date false +\justification true +\use_refstyle 1 +\use_minted 0 +\index Index +\shortcut idx +\color #008000 +\end_index +\secnumdepth 3 +\tocdepth 3 +\paragraph_separation indent +\paragraph_indentation default +\is_math_indent 0 +\math_numbering_side default +\quotes_style swiss +\dynamic_quotes 0 +\papercolumns 1 +\papersides 1 +\paperpagestyle default +\tracking_changes false +\output_changes false +\html_math_output 0 +\html_css_as_file 0 +\html_be_strict false +\end_header + +\begin_body + +\begin_layout Standard +Las expresiones, numeradas, están dentro de una caja, que se representa + con los tres bordes de arriba, abajo y a la izquierda (a la derecha del + número de línea). + La caja principal no se suele representar. + Si se usa una +\emph on +Hipótesis +\emph default +, se crea una nueva caja (dentro de otra), y en cada caja las +\emph on +Premisas +\emph default + o +\emph on +Hipótesis +\emph default + van al principio y la última línea es la conclusión. + Cada caja representa una deducción ( +\begin_inset Formula $\vdash$ +\end_inset + +). +\end_layout + +\begin_layout Section +Reglas +\end_layout + +\begin_layout Standard +\align center +\begin_inset Tabular + + + + + + + +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +Eliminación de +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +Introducción de +\end_layout + +\end_inset + + + + +\begin_inset Text + +\begin_layout Plain Layout +la conjunción +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $E_{\land}:\frac{\vdash\alpha\land\beta}{\vdash\alpha},\frac{\vdash\alpha\land\beta}{\vdash\beta}$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $I_{\land}:\frac{\vdash\alpha\,\vdash\beta}{\vdash\alpha\land\beta}$ +\end_inset + + +\end_layout + +\end_inset + + + + +\begin_inset Text + +\begin_layout Plain Layout +la disyunción +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\underset{\text{Prueba por casos}}{E_{\lor}:\frac{\vdash\alpha\lor\beta\,\vdash(\alpha\vdash\gamma)\,\vdash(\beta\vdash\gamma)}{\vdash\gamma}}$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $I_{\lor}:\frac{\vdash\alpha}{\vdash\alpha\lor\beta},\frac{\vdash\alpha}{\vdash\beta\lor\alpha}$ +\end_inset + + +\end_layout + +\end_inset + + + + +\begin_inset Text + +\begin_layout Plain Layout +la implicación +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\underset{\text{Modus Ponens}}{E_{\rightarrow}:\frac{\vdash\alpha\rightarrow\beta\,\vdash\alpha}{\vdash\beta}}$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\underset{\text{Teorema de la Deducción}}{I_{\rightarrow}:\frac{\vdash(\alpha\vdash\beta)}{\vdash\alpha\rightarrow\beta}}$ +\end_inset + + +\end_layout + +\end_inset + + + + +\begin_inset Text + +\begin_layout Plain Layout +la doble implicación +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $E_{\leftrightarrow}:\frac{\vdash(\alpha\leftrightarrow\beta)}{\vdash(\alpha\rightarrow\beta)},\frac{\vdash(\alpha\leftrightarrow\beta)}{\vdash(\beta\rightarrow\alpha)}$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $I_{\leftrightarrow}:\frac{\vdash(\alpha\rightarrow\beta)\,\vdash(\beta\rightarrow\alpha)}{\vdash(\alpha\leftrightarrow\beta)}$ +\end_inset + + +\end_layout + +\end_inset + + + + +\begin_inset Text + +\begin_layout Plain Layout +la negación +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\underset{\text{Reducción al absurdo}}{E_{\neg}:\frac{\vdash(\neg\alpha\vdash\beta\land\neg\beta)}{\vdash\alpha}}$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\underset{\text{Reducción al absurdo}}{I_{\neg}:\frac{\vdash(\alpha\vdash\beta\land\neg\beta)}{\vdash\neg\alpha}}$ +\end_inset + + +\end_layout + +\end_inset + + + + +\begin_inset Text + +\begin_layout Plain Layout +la doble negación +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $E_{\neg\neg}:\frac{\vdash\neg\neg\alpha}{\vdash\alpha}$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset + + + + +\begin_inset Text + +\begin_layout Plain Layout +la contradicción +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $CONTRA:\frac{\vdash\alpha\,\vdash\neg\alpha}{\vdash\beta}$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset + + + + +\end_inset + + +\end_layout + +\begin_layout Standard +También la iteración: +\begin_inset Formula $IT:\frac{\vdash\alpha}{\vdash\alpha}$ +\end_inset + +, que se usa cuando la hipótesis de una caja es la conclusión, dado que + deben estar en líneas distintas. +\end_layout + +\end_body +\end_document diff --git a/fli/n5.lyx b/fli/n5.lyx new file mode 100644 index 0000000..e887da2 --- /dev/null +++ b/fli/n5.lyx @@ -0,0 +1,660 @@ +#LyX 2.3 created this file. For more info see http://www.lyx.org/ +\lyxformat 544 +\begin_document +\begin_header +\save_transient_properties true +\origin unavailable +\textclass book +\use_default_options true +\maintain_unincluded_children false +\language spanish +\language_package default +\inputencoding auto +\fontencoding global +\font_roman "default" "default" +\font_sans "default" "default" +\font_typewriter "default" "default" +\font_math "auto" "auto" +\font_default_family default +\use_non_tex_fonts false +\font_sc false +\font_osf false +\font_sf_scale 100 100 +\font_tt_scale 100 100 +\use_microtype false +\use_dash_ligatures true +\graphics default +\default_output_format default +\output_sync 0 +\bibtex_command default +\index_command default +\paperfontsize default +\spacing single +\use_hyperref false +\papersize default +\use_geometry false +\use_package amsmath 1 +\use_package amssymb 1 +\use_package cancel 1 +\use_package esint 1 +\use_package mathdots 1 +\use_package mathtools 1 +\use_package mhchem 1 +\use_package stackrel 1 +\use_package stmaryrd 1 +\use_package undertilde 1 +\cite_engine basic +\cite_engine_type default +\biblio_style plain +\use_bibtopic false +\use_indices false +\paperorientation portrait +\suppress_date false +\justification true +\use_refstyle 1 +\use_minted 0 +\index Index +\shortcut idx +\color #008000 +\end_index +\secnumdepth 3 +\tocdepth 3 +\paragraph_separation indent +\paragraph_indentation default +\is_math_indent 0 +\math_numbering_side default +\quotes_style swiss +\dynamic_quotes 0 +\papercolumns 1 +\papersides 1 +\paperpagestyle default +\tracking_changes false +\output_changes false +\html_math_output 0 +\html_css_as_file 0 +\html_be_strict false +\end_header + +\begin_body + +\begin_layout Section +Conjuntos +\end_layout + +\begin_layout Standard +Una +\series bold +categoría +\series default + o +\series bold +conjunto +\series default + es una colección no ordenada de +\series bold +elementos +\series default +. + Se dice que un elemento +\begin_inset Formula $x$ +\end_inset + + pertenece al conjunto +\begin_inset Formula $C$ +\end_inset + +, y se representa como +\begin_inset Formula $x\in C$ +\end_inset + + (negación: +\begin_inset Formula $x\notin C$ +\end_inset + +) o +\begin_inset Formula $C(x)$ +\end_inset + +. + Podemos definir un conjunto por extensión ( +\begin_inset Formula $C=\{x_{1},x_{2},\dots\}$ +\end_inset + +), intensión ( +\begin_inset Formula $C=\{x|P(x)\}$ +\end_inset + +) o recursión ( +\begin_inset Formula $C=\{x|R(x)\}$ +\end_inset + +). +\end_layout + +\begin_layout Itemize + +\series bold +Igualdad: +\series default + +\begin_inset Formula $A=B:\iff(x\in A\iff x\in B)$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Inclusión: +\series default + +\begin_inset Formula $A\subseteq B:\iff(x\in A\implies x\in B)$ +\end_inset + + (negación: +\begin_inset Formula $A\nsubseteq B$ +\end_inset + +). +\end_layout + +\begin_layout Itemize + +\series bold +Inclusión estricta: +\series default + +\begin_inset Formula $A\subsetneq B:\iff(A\subseteq B\text{ y }A\neq B$ +\end_inset + +). +\end_layout + +\begin_layout Itemize + +\series bold +Conjunto total +\series default + o +\series bold +universo: +\series default + +\begin_inset Formula ${\cal U}$ +\end_inset + +, el mayor conjunto que podemos considerar para un estudio. +\end_layout + +\begin_layout Itemize + +\series bold +Conjunto vacío: +\series default + +\begin_inset Formula $\emptyset=\{\}$ +\end_inset + +, sin elementos. +\end_layout + +\begin_layout Itemize + +\series bold +Partes: +\series default + +\begin_inset Formula ${\cal P}(X)=\{A|A\subseteq X\}$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Unión: +\series default + +\begin_inset Formula $A\cup B:=\{x|x\in A\text{ ó }x\in B\}$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Intersección: +\series default + +\begin_inset Formula $A\cap B:=\{x|x\in A\text{ y }x\in B\}$ +\end_inset + +. + Si +\begin_inset Formula $A\cap B=\emptyset$ +\end_inset + +, +\begin_inset Formula $A$ +\end_inset + + y +\begin_inset Formula $B$ +\end_inset + + son +\series bold +disjuntos +\series default +. +\end_layout + +\begin_layout Itemize + +\series bold +Diferencia: +\series default + +\begin_inset Formula $A-B:=A\backslash B:=\{x|x\in A\text{ y }x\notin B\}$ +\end_inset + + +\end_layout + +\begin_layout Itemize + +\series bold +Complemento: +\series default + +\begin_inset Formula $\overline{A}:=A^{\complement}:={\cal U}\backslash A$ +\end_inset + +. +\end_layout + +\begin_layout Standard +Un +\series bold +diagrama de Euler +\series default + representa los conjuntos como círculos bien unos dentro de otros, separados + o intersecados, indicando de esta forma sus relaciones. + Un +\series bold +diagrama de Venn +\series default + representa los conjuntos como círculos todos intersecados entre sí, con + las partes no vacías sombreadas. +\end_layout + +\begin_layout Standard +Una +\series bold +familia de conjuntos +\series default + +\begin_inset Formula ${\cal A}$ +\end_inset + + es un conjunto formado solo por conjuntos, y es una +\series bold +partición +\series default + de +\begin_inset Formula $A$ +\end_inset + + si y sólo si +\begin_inset Formula $\bigcup{\cal A}=A$ +\end_inset + + y si para todo +\begin_inset Formula $B,C\in{\cal A}$ +\end_inset + + con +\begin_inset Formula $B\neq C$ +\end_inset + + se tiene que +\begin_inset Formula $B\cap C=\emptyset$ +\end_inset + +. +\end_layout + +\begin_layout Section +Sintaxis +\end_layout + +\begin_layout Standard +Extensión de la lógica proposicional. + Las proposiciones atómicas tienen la forma +\begin_inset Formula $P(x)$ +\end_inset + +, donde +\begin_inset Formula $P$ +\end_inset + + es una categoría y +\begin_inset Formula $x$ +\end_inset + + una variable (ambas conjuntos de letras latinas), y se leen +\begin_inset Quotes cld +\end_inset + + +\begin_inset Formula $x$ +\end_inset + + es +\begin_inset Formula $P$ +\end_inset + + +\begin_inset Quotes crd +\end_inset + +. + Además, se añaden los cuantificadores +\begin_inset Formula $\forall x$ +\end_inset + + (para todo +\begin_inset Formula $x$ +\end_inset + +) y +\begin_inset Formula $\exists x$ +\end_inset + + (existe +\begin_inset Formula $x$ +\end_inset + +), donde +\begin_inset Formula $x$ +\end_inset + + puede ser cualquier variable. + Estos tienen la misma prioridad que la negación. + Las proposiciones compuestas se forman mediante cuatro +\series bold +formas normales: +\end_layout + +\begin_layout Itemize + +\series bold +Universal afirmativa: +\series default + +\begin_inset Formula $\forall x(P(x)\rightarrow Q(x))$ +\end_inset + +; +\begin_inset Quotes cld +\end_inset + +todo +\begin_inset Formula $P$ +\end_inset + + es +\begin_inset Formula $Q$ +\end_inset + + +\begin_inset Quotes crd +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Universal negativa: +\series default + +\begin_inset Formula $\forall x(P(x)\rightarrow\neg Q(x))$ +\end_inset + +; +\begin_inset Quotes cld +\end_inset + +ningún +\begin_inset Formula $P$ +\end_inset + + es +\begin_inset Formula $Q$ +\end_inset + + +\begin_inset Quotes crd +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Existencial afirmativa: +\series default + +\begin_inset Formula $\exists x(P(x)\land Q(x))$ +\end_inset + +; +\begin_inset Quotes cld +\end_inset + +algún +\begin_inset Formula $P$ +\end_inset + + es +\begin_inset Formula $Q$ +\end_inset + + +\begin_inset Quotes crd +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Existencial negativa: +\series default + +\begin_inset Formula $\exists x(P(x)\land\neg Q(x))$ +\end_inset + +; +\begin_inset Quotes cld +\end_inset + +algún +\begin_inset Formula $P$ +\end_inset + + no es +\begin_inset Formula $Q$ +\end_inset + + +\begin_inset Quotes crd +\end_inset + +. +\end_layout + +\begin_layout Section +Evaluación +\end_layout + +\begin_layout Standard +Para evaluar una proposición en LC interpretada en un mundo +\begin_inset Formula ${\cal M}$ +\end_inset + +: +\end_layout + +\begin_layout Enumerate +Definimos +\begin_inset Formula ${\cal U}$ +\end_inset + + como el conjunto de todos los elementos que aparecen en +\begin_inset Formula ${\cal M}$ +\end_inset + +. +\end_layout + +\begin_layout Enumerate +Identificamos cada categoría +\begin_inset Formula $P$ +\end_inset + + con un conjunto +\begin_inset Formula $P_{{\cal M}}$ +\end_inset + + del mundo. + El resultado es la +\series bold +interpretación +\series default + +\begin_inset Formula $I=\{P\mapsto P_{{\cal M}},\dots\}$ +\end_inset + +. +\end_layout + +\begin_layout Enumerate +Evaluamos el valor de verdad de la proposición a partir de la interpretación. + Para ello: +\end_layout + +\begin_deeper +\begin_layout Enumerate +Si encontramos un +\begin_inset Formula $\forall x\alpha[x]$ +\end_inset + +, decimos que esto es verdad si para cualquier +\begin_inset Formula $x\looparrowright d$ +\end_inset + + se cumple +\begin_inset Formula $V(\alpha[d])=V$ +\end_inset + +. + Aquí, +\begin_inset Formula $\alpha[d]\equiv\{\alpha[x]\}_{d/x}$ +\end_inset + + el resultado de aplicar la +\series bold +sustitución +\series default + +\begin_inset Formula $\{d/x\}$ +\end_inset + +. + Entonces comprobamos +\begin_inset Formula $V(\alpha[d])$ +\end_inset + + para todo +\begin_inset Formula $x\looparrowright d$ +\end_inset + + ( +\series bold +asignación +\series default +) con +\begin_inset Formula $d\in{\cal U}$ +\end_inset + + hasta encontrar un caso donde +\begin_inset Formula $V(\alpha[d])=F$ +\end_inset + + (con lo que +\begin_inset Formula $V(\forall x\alpha[x])=F$ +\end_inset + +) o llegar a que en todos +\begin_inset Formula $V(\alpha[d])=V$ +\end_inset + + (con lo que +\begin_inset Formula $V(\forall x\alpha[x])=V$ +\end_inset + +). +\end_layout + +\begin_layout Enumerate +Si encontramos un +\begin_inset Formula $\exists x\alpha[x]$ +\end_inset + + decimos que esto es verdad si encontramos un +\begin_inset Formula $x\looparrowright d$ +\end_inset + + para el que +\begin_inset Formula $V(\alpha[d])=V$ +\end_inset + +. + Entonces comprobamos +\begin_inset Formula $V(\alpha[d])$ +\end_inset + + para todo +\begin_inset Formula $x\looparrowright d$ +\end_inset + + con +\begin_inset Formula $d\in{\cal U}$ +\end_inset + + hasta encontrar un caso donde +\begin_inset Formula $V(\alpha[d])=V$ +\end_inset + + (con lo que +\begin_inset Formula $V(\exists x\alpha[x])=V$ +\end_inset + +) o llegar a que todos son falsos (con lo que +\begin_inset Formula $V(\exists x\alpha[x])=F$ +\end_inset + +). +\end_layout + +\end_deeper +\end_body +\end_document diff --git a/fli/n6.lyx b/fli/n6.lyx new file mode 100644 index 0000000..f89c446 --- /dev/null +++ b/fli/n6.lyx @@ -0,0 +1,1406 @@ +#LyX 2.3 created this file. For more info see http://www.lyx.org/ +\lyxformat 544 +\begin_document +\begin_header +\save_transient_properties true +\origin unavailable +\textclass book +\use_default_options true +\maintain_unincluded_children false +\language spanish +\language_package default +\inputencoding auto +\fontencoding global +\font_roman "default" "default" +\font_sans "default" "default" +\font_typewriter "default" "default" +\font_math "auto" "auto" +\font_default_family default +\use_non_tex_fonts false +\font_sc false +\font_osf false +\font_sf_scale 100 100 +\font_tt_scale 100 100 +\use_microtype false +\use_dash_ligatures true +\graphics default +\default_output_format default +\output_sync 0 +\bibtex_command default +\index_command default +\paperfontsize default +\spacing single +\use_hyperref false +\papersize default +\use_geometry false +\use_package amsmath 1 +\use_package amssymb 1 +\use_package cancel 1 +\use_package esint 1 +\use_package mathdots 1 +\use_package mathtools 1 +\use_package mhchem 1 +\use_package stackrel 1 +\use_package stmaryrd 1 +\use_package undertilde 1 +\cite_engine basic +\cite_engine_type default +\biblio_style plain +\use_bibtopic false +\use_indices false +\paperorientation portrait +\suppress_date false +\justification true +\use_refstyle 1 +\use_minted 0 +\index Index +\shortcut idx +\color #008000 +\end_index +\secnumdepth 3 +\tocdepth 3 +\paragraph_separation indent +\paragraph_indentation default +\is_math_indent 0 +\math_numbering_side default +\quotes_style swiss +\dynamic_quotes 0 +\papercolumns 1 +\papersides 1 +\paperpagestyle default +\tracking_changes false +\output_changes false +\html_math_output 0 +\html_css_as_file 0 +\html_be_strict false +\end_header + +\begin_body + +\begin_layout Section +Relaciones +\end_layout + +\begin_layout Standard +La lógica de primer orden (L1) extiende la lógica categórica permitiendo + expresar relaciones fuera de las formas normales y relaciones de varios + objetos. + Podemos distinguir: +\end_layout + +\begin_layout Itemize + +\series bold +Categorías: +\series default + +\begin_inset Quotes cld +\end_inset + + +\begin_inset Formula $x$ +\end_inset + + es +\begin_inset Formula $P$ +\end_inset + + +\begin_inset Quotes crd +\end_inset + +, +\begin_inset Formula $x\in P$ +\end_inset + +, +\begin_inset Formula $P(r)$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Relaciones binarias: +\series default + +\begin_inset Quotes cld +\end_inset + + +\begin_inset Formula $x$ +\end_inset + + e +\begin_inset Formula $y$ +\end_inset + + son +\begin_inset Formula $R$ +\end_inset + + +\begin_inset Quotes crd +\end_inset + +, +\begin_inset Quotes cld +\end_inset + + +\begin_inset Formula $x$ +\end_inset + + se relaciona con +\begin_inset Formula $y$ +\end_inset + + +\begin_inset Quotes crd +\end_inset + +, +\begin_inset Formula $(x,y)\in R$ +\end_inset + +, +\begin_inset Formula $R(x,y)$ +\end_inset + +, +\begin_inset Formula $xRy$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Relaciones +\series default + de cualquier orden: +\begin_inset Formula $(x_{1},\dots,x_{n})\in S$ +\end_inset + +, +\begin_inset Formula $S(x_{1},\dots,x_{n})$ +\end_inset + +. + Se dice que +\begin_inset Formula $S$ +\end_inset + + tiene +\series bold +aridad +\series default + +\begin_inset Formula $n$ +\end_inset + +, o que es una relación +\series bold + +\begin_inset Formula $n$ +\end_inset + +-aria +\series default +, lo que se representa por +\begin_inset Formula $S/n$ +\end_inset + +. + En general, +\begin_inset Formula $Q$ +\end_inset + + es una relación +\begin_inset Formula $n$ +\end_inset + +-aria entre +\begin_inset Formula $A_{1},\dots,A_{n}$ +\end_inset + + si +\begin_inset Formula $Q\subseteq\prod_{i=1}^{n}A_{i}$ +\end_inset + +. + Si +\begin_inset Formula $\forall i,A_{i}=A$ +\end_inset + +, entonces +\begin_inset Formula $\prod_{i=1}^{n}A_{i}=A^{n}$ +\end_inset + +. +\end_layout + +\begin_layout Standard +En relaciones con aridad +\begin_inset Formula $n\geq2$ +\end_inset + +, se define el +\series bold +dominio +\series default + como +\begin_inset Formula $\text{Dom}(R)=\{(x_{1},\dots,x_{n-1})|\exists x_{n}:(x_{1},\dots,x_{n})\in R\}$ +\end_inset + + (si la aridad es +\begin_inset Formula $2$ +\end_inset + +, entonces +\begin_inset Formula $\text{Dom}(R)=\{x|\exists y:xRy\}$ +\end_inset + +), y el +\series bold +rango +\series default + como +\begin_inset Formula $\text{Ran}(R)=\{x_{n}|\exists(x_{1},\dots,x_{n-1}):(x_{1},\dots,x_{n})\in R\}$ +\end_inset + + (si la aridad es +\begin_inset Formula $2$ +\end_inset + +, entonces +\begin_inset Formula $\text{Ran}(R)=\{y|\exists x:xRy\}$ +\end_inset + +. + El +\series bold +campo +\series default + de +\begin_inset Formula $R$ +\end_inset + + se define como +\begin_inset Formula $\text{Campo}(R)=\text{Dom}(R)\cup\text{Ran}(R)$ +\end_inset + +. + Representaciones: +\end_layout + +\begin_layout Itemize + +\series bold +Cartesiana: +\series default + Similar a una función, con el conjunto inicial en el eje horizontal. + Se marcan los puntos que están en +\begin_inset Formula $R$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Tabular: +\series default + Como la cartesiana pero en una tabla. + En cada celda se pone un +\begin_inset Formula $1$ +\end_inset + + si el producto de tipos está en +\begin_inset Formula $R$ +\end_inset + +, un +\begin_inset Formula $0$ +\end_inset + + si no está y se deja en blanco si no lo sabemos. +\end_layout + +\begin_layout Itemize + +\series bold +Mediante digrafo: +\series default + Se representa a la izquierda el conjunto inicial y a la derecha el final, + y las relaciones se representan con flechas entre elementos de cada. +\end_layout + +\begin_layout Itemize + +\series bold +Grafo dirigido: +\series default + Se representa +\begin_inset Formula ${\cal U}$ +\end_inset + + y se indican las relaciones binarias con flechas. +\end_layout + +\begin_layout Standard +Una relación +\begin_inset Formula $n$ +\end_inset + +-aria +\begin_inset Formula $f$ +\end_inset + + es una +\series bold +función +\series default + si y sólo si para cada elemento +\begin_inset Formula $x\in\text{Dom}(f)$ +\end_inset + + existe un único +\begin_inset Formula $y\in\text{Ran}(f)$ +\end_inset + + que se relacione con él. + Se escribe +\begin_inset Formula $f(x)=y$ +\end_inset + +, y la función se representa como +\begin_inset Formula $f:\prod_{i=1}^{n-1}A_{i}\rightarrow A_{n}$ +\end_inset + +. + Es +\series bold +inyectiva +\series default + si +\begin_inset Formula $f(x)=f(x')\implies x=x'$ +\end_inset + +, +\series bold +suprayectiva +\series default + si +\begin_inset Formula $\text{Ran}(f)=A_{n}$ +\end_inset + + y +\series bold +biyectiva +\series default + si es inyectiva y suprayectiva. + Definimos la aridad de +\begin_inset Formula $f$ +\end_inset + + como función como +\begin_inset Formula $n-1$ +\end_inset + +. +\end_layout + +\begin_layout Standard +\begin_inset Note Comment +status open + +\begin_layout Plain Layout +Tipos de relaciones: +\end_layout + +\begin_layout Itemize + +\series bold +Reflexiva: +\series default + +\begin_inset Formula $\forall a\in A,aRa$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Irreflexiva: +\series default + +\begin_inset Formula $\forall a\in A,a\not Ra$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Serial: +\series default + +\begin_inset Formula $\forall a\in A,\exists b\in A:aRb$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Simétrica: +\series default + +\begin_inset Formula $\forall a,b\in A,(aRb\implies bRa)$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Asimétrica: +\series default + +\begin_inset Formula $\forall a,b\in A,(aRb\implies b\not Ra)$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Antisimétrica: +\series default + +\begin_inset Formula $\forall a,b\in A,(aRb\land bRa\implies a=b)$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Transitiva: +\series default + +\begin_inset Formula $\forall a,b,c\in A,(aRb\land bRc\implies aRc)$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Intransitiva: +\series default + +\begin_inset Formula $\forall a,b,c\in A,(aRb\land bRc\implies a\not Rc)$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Negativamente transitiva: +\series default + +\begin_inset Formula $\forall a,b,c\in A,(a\not Rb\land b\not Rc\implies a\not Rc)$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Completa: +\series default + +\begin_inset Formula $\forall a,b\in A,(aRb\lor bRa)$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Euclídea: +\series default + +\begin_inset Formula $\forall a,b,c\in A,(aRb\land aRc\implies bRc)$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Incestuosa: +\series default + +\begin_inset Formula $\forall a,b,c\in A,(aRb\land aRc\implies\exists d\in A:(bRd\land cRd))$ +\end_inset + +. +\end_layout + +\begin_layout Plain Layout +Dada +\begin_inset Formula $R\subseteq A\times B$ +\end_inset + +, su +\series bold +relación inversa +\series default + es +\begin_inset Formula $R^{-1}$ +\end_inset + + con +\begin_inset Formula $xR^{-1}y:\iff yRx$ +\end_inset + +. + Dada +\begin_inset Formula $R\subseteq A\times A$ +\end_inset + +: +\end_layout + +\begin_layout Itemize +Su +\series bold +relación complementaria +\series default + es +\begin_inset Formula $R^{\complement}$ +\end_inset + + con +\begin_inset Formula $xR^{\complement}y:\iff x\not Ry$ +\end_inset + +. +\end_layout + +\begin_layout Itemize +Su +\series bold +relación simétrica +\series default + es +\begin_inset Formula $\overline{R}=R^{-1}$ +\end_inset + + con +\begin_inset Formula $x\overline{R}y:\iff yRx$ +\end_inset + +. +\end_layout + +\begin_layout Itemize +Su +\series bold +relación dual +\series default + es +\begin_inset Formula $R^{d}$ +\end_inset + + con +\begin_inset Formula $aR^{d}b:\iff b\not Ra$ +\end_inset + +. +\end_layout + +\begin_layout Plain Layout +Una relación de equivalencia es aquella reflexiva, simétrica y transitiva. + Sea +\begin_inset Formula $(A,\sim)$ +\end_inset + + de equivalencia, podemos definir la clase de equivalencia de +\begin_inset Formula $x$ +\end_inset + +, +\begin_inset Formula $[x]$ +\end_inset + +, como el conjunto de todos los elementos que se relacionan con +\begin_inset Formula $[x]$ +\end_inset + +. + +\begin_inset Formula $y\in[x]\implies[y]=[x]$ +\end_inset + +, y decimos que +\begin_inset Formula $y$ +\end_inset + + es un representante de la clase. + El conjunto cociente es el formado por todas las clases de equivalencia, + y se escribe +\begin_inset Formula $A/\sim=\{[x]|x\in A\}$ +\end_inset + +. +\end_layout + +\end_inset + + +\end_layout + +\begin_layout Section +Sintaxis +\end_layout + +\begin_layout Itemize + +\series bold +Proposición atómica: +\series default + +\begin_inset Formula $V$ +\end_inset + +, +\begin_inset Formula $F$ +\end_inset + + o un predicado. +\end_layout + +\begin_layout Itemize + +\series bold +Predicado: +\series default + Secuencia de letras latinas que representa una relación, seguida de una + serie de términos: +\begin_inset Formula $R(t_{1},\dots,t_{n})$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Término: +\series default + Constante que representa un objeto definido, variable o función. +\end_layout + +\begin_layout Itemize + +\series bold +Constante: +\series default + Secuencia de letras latinas que representa a un objeto definido (salvo + +\begin_inset Formula $V$ +\end_inset + + y +\begin_inset Formula $F$ +\end_inset + +). +\end_layout + +\begin_layout Itemize + +\series bold +Variable: +\series default + Secuencia de letras latinas que representa a un objeto indefinido. + Puede estar +\series bold +ligada +\series default + a un cuantificador, y entonces es igual al resto de variables ligadas al + mismo, o +\series bold +libre +\series default +, en cuyo caso puede representar cualquier cosa. +\end_layout + +\begin_layout Itemize + +\series bold +Función: +\series default + Secuencia de letras latinas que representa una función, seguida de una + serie de términos: +\begin_inset Formula $f(t_{1},\dots,t_{n})$ +\end_inset + +. +\end_layout + +\begin_layout Standard +La construcción de f.b.f es igual que en L0, pero cambiando la forma de las + proposiciones atómicas y añadiendo que si +\begin_inset Formula $\alpha$ +\end_inset + + es f.b.f. + también lo son +\begin_inset Formula $(\forall x\alpha)$ +\end_inset + + y +\begin_inset Formula $(\exists x\alpha)$ +\end_inset + +. + Una f.b.f. + es +\series bold +cerrada +\series default + si todas las variables están ligadas y +\series bold +abierta +\series default + en otro caso. +\end_layout + +\begin_layout Section +Interpretación y asignación +\end_layout + +\begin_layout Standard +Una +\series bold +interpretación +\series default + de +\begin_inset Formula $\alpha$ +\end_inset + + en un +\series bold +mundo +\series default + +\begin_inset Formula $\mathbb{M}$ +\end_inset + + es una cuaterna +\begin_inset Formula ${\cal I}_{\alpha}=(\mathbb{D},{\cal C}_{\mathbb{D}},{\cal F}_{\mathbb{D}},{\cal R}_{\mathbb{D}})$ +\end_inset + + donde +\begin_inset Formula $\mathbb{D}$ +\end_inset + + es un conjunto no vacío de objetos, llamado dominio, +\begin_inset Formula ${\cal C}_{\mathbb{D}}$ +\end_inset + + es un conjunto de objetos concretos ( +\begin_inset Formula ${\cal C_{\alpha}\mapsto{\cal C}_{\mathbb{D}}}$ +\end_inset + +), +\begin_inset Formula ${\cal F}_{\mathbb{D}}$ +\end_inset + + de funciones concretas ( +\begin_inset Formula $f_{\alpha}\mapsto f_{\mathbb{D}}$ +\end_inset + +) y +\begin_inset Formula ${\cal R}_{\mathbb{D}}$ +\end_inset + + de relaciones concretas ( +\begin_inset Formula $R_{\alpha}\mapsto R_{\mathbb{D}}$ +\end_inset + +). + La +\series bold +signatura +\series default + es el conjunto de todos los predicados y funciones, indicando su aridad. +\end_layout + +\begin_layout Standard +Una asignación de variables es una función +\begin_inset Formula $\sigma_{{\cal I}_{\alpha}}:{\cal V}\rightarrow\mathbb{D}$ +\end_inset + + que relaciona cada variable de +\begin_inset Formula $\alpha$ +\end_inset + + con un elemento del dominio, y definimos +\begin_inset Formula $\sigma_{{\cal I}_{\alpha}|x\looparrowright d}$ +\end_inset + + a la asignación definida igual que +\begin_inset Formula $\sigma_{{\cal I}_{\alpha}}$ +\end_inset + + pero asignando a +\begin_inset Formula $x$ +\end_inset + + el objeto +\begin_inset Formula $d$ +\end_inset + +. +\end_layout + +\begin_layout Standard +Una +\series bold +asignación de valores de verdad +\series default + +\begin_inset Formula $v_{\sigma_{{\cal I}_{\alpha}}}:{\cal P_{\alpha}\rightarrow\mathbb{B}}$ +\end_inset + + asigna un valor de verdad a cada elemento atómico de +\begin_inset Formula $\alpha$ +\end_inset + +. + Así, +\begin_inset Formula $v(R_{\alpha}(t_{1},\dots,t_{n}))=V\iff(d_{1},\dots,d_{n})\in R_{\mathbb{D}}$ +\end_inset + +, donde si +\begin_inset Formula $t_{i}$ +\end_inset + + es constante entonces +\begin_inset Formula $d_{i}=t_{i}$ +\end_inset + +, si +\begin_inset Formula $t_{i}=f(x_{1},\dots,x_{n})$ +\end_inset + + entonces +\begin_inset Formula $d_{i}$ +\end_inset + + es el único +\begin_inset Formula $y$ +\end_inset + + tal que +\begin_inset Formula $(x_{1},\dots,x_{n},y)\in f$ +\end_inset + +, y si es variable entonces depende de la +\series bold +asignación +\series default +. +\end_layout + +\begin_layout Standard +La +\series bold +evaluación +\series default + de una oración +\begin_inset Formula $\alpha$ +\end_inset + + se hace igual que en LC, pero partiendo de esta asignación de valores de + verdad. + También se puede hacer mediante tablas de verdad, que en L1 sólo evalúan + una interpretación a la vez: +\end_layout + +\begin_layout Enumerate +Se introduce una columna por variable, dividida en una fila por cada valor + del dominio. + Puede ser necesario considerar aquí todas las posibles combinaciones de + variables. +\end_layout + +\begin_layout Enumerate +Se introduce una columna por cada función que aparece en la oración, y se + evalúa de acuerdo al valor de la variable dado. +\end_layout + +\begin_layout Enumerate +Se introducen las filas correspondientes a la fórmula, indicando el orden + de evaluación. + Un cuantificador que no está dentro de otro ocupa la fila completa, pero + su contenido se divide en una fila por cada posible asignación de la variable. + Una vez se conoce el valor del cuantificador no es necesario evaluar el + resto de asignaciones, pero es importante justificar los valores de verdad + de los predicados (ejemplos: +\begin_inset Formula $V:(a,b)\in P_{{\cal M}}$ +\end_inset + +; +\begin_inset Formula $F:(c,a)\notin Q_{{\cal M}}$ +\end_inset + +). +\end_layout + +\begin_layout Standard +Este método es impráctico, por lo que no se usa. +\end_layout + +\begin_layout Section +Sustituciones +\end_layout + +\begin_layout Standard +Una +\series bold +sustitución +\series default + es una expresión +\begin_inset Formula $s=\{t_{1}/v_{1},\dots,t_{n}/v_{n}\}$ +\end_inset + + que indica que toda ocurrencia de cada +\begin_inset Formula $v_{i}$ +\end_inset + + se debe sustituir por el término +\begin_inset Formula $t_{i}$ +\end_inset + +. + Todas las sustituciones se hacen simultáneamente. +\end_layout + +\begin_layout Standard +Una +\series bold +particularización por sustitución +\series default + consiste en sustituir sus variables por términos. + Escribimos +\begin_inset Formula $Ps$ +\end_inset + + como la particularización de la expresión +\begin_inset Formula $P$ +\end_inset + + según la sustitución +\begin_inset Formula $s$ +\end_inset + +. +\end_layout + +\begin_layout Itemize +En una +\series bold +particularización básica +\series default +, los términos son constantes. +\end_layout + +\begin_layout Itemize +En una +\series bold +particularización alfabética +\series default +, los términos son otras variables. +\end_layout + +\begin_layout Standard + +\series bold +Composición de sustituciones: +\series default + Dadas +\begin_inset Formula $s=\{a_{1}/x_{1},\dots,a_{n}/x_{n}\}$ +\end_inset + + y +\begin_inset Formula $t=\{b_{1}/y_{1},\dots,b_{m}/y_{m}\}$ +\end_inset + + con +\begin_inset Formula $X$ +\end_inset + + e +\begin_inset Formula $Y$ +\end_inset + + los conjuntos de variables sustituidas respectivamente según +\begin_inset Formula $s$ +\end_inset + + y +\begin_inset Formula $t$ +\end_inset + +, +\begin_inset Formula $s\cdot t=\{(a_{i}t)/x_{i}|x_{i}\neq a_{i}t\}\cup\{b_{i}/y_{i}|y_{i}\in Y\backslash X\}$ +\end_inset + +, donde +\begin_inset Formula $a_{i}t$ +\end_inset + + es la particularización de +\begin_inset Formula $a_{i}$ +\end_inset + + según +\begin_inset Formula $t$ +\end_inset + +. +\end_layout + +\begin_layout Section +Equivalencias +\end_layout + +\begin_layout Standard +\align center +\begin_inset Tabular + + + + + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg\exists x\alpha[x]\equiv\forall x\neg\alpha[x]$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg\forall x\alpha[x]\equiv\exists x\neg\alpha[x]$ +\end_inset + + +\end_layout + +\end_inset + + + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\forall x(\alpha[x]\land\beta[x])\equiv\forall x\alpha[x]\land\forall x\beta[x]$ +\end_inset + + +\end_layout + +\end_inset + + +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\exists x(\alpha[x]\lor\beta[x])\equiv\exists x\alpha[x]\lor\exists x\beta[x]$ +\end_inset + + +\end_layout + +\end_inset + + + + +\end_inset + + +\end_layout + +\begin_layout Standard +También, tanto en L1 como en LC, podemos sustituir el nombre de una variable + por otro siempre que lo cambiemos en el cuantificador al que está ligado + y en todos los símbolos ligados al mismo cuantificador (o bien la variable + sea libre), y al hacerlo todas las variables de la oración sigan ligadas + al mismo cuantificador de partida (o sigan libres). +\end_layout + +\begin_layout Section +Satisfacibilidad +\end_layout + +\begin_layout Standard +Podemos comprobar la satisfacibilidad de una oración mediante tableaux. + Añadimos dos tipos de reglas: +\end_layout + +\begin_layout Itemize +\begin_inset Formula $\gamma$ +\end_inset + + +\series bold +-reglas +\series default +: +\begin_inset Formula $\forall x\alpha[x]\mapsto\alpha[C],\forall x\alpha[x]$ +\end_inset + +; +\begin_inset Formula $\neg\exists x\alpha[x]\mapsto\neg\alpha[C],\neg\exists x\alpha[x]$ +\end_inset + +. + La sustitución +\begin_inset Formula $\{C/x\}$ +\end_inset + + se hace sobre una constante +\begin_inset Formula $C$ +\end_inset + + existente. + Si no existe ninguna, debemos suponer una nueva. + El +\begin_inset Formula $\forall x\alpha[x]$ +\end_inset + + resultante no hace referencia a +\begin_inset Formula $C$ +\end_inset + +, de modo que se debe escribir una lista debajo de cada expresión de este + tipo ( +\begin_inset Formula $L=\{\dots\}$ +\end_inset + +) con los elementos a los que sí hace referencia. +\end_layout + +\begin_layout Itemize +\begin_inset Formula $\delta$ +\end_inset + + +\series bold +-reglas +\series default +: +\begin_inset Formula $\exists x\alpha[x]\mapsto\alpha[C]$ +\end_inset + +; +\begin_inset Formula $\neg\forall x\alpha[x]\mapsto\neg\alpha[C]$ +\end_inset + +. + La sustitución +\begin_inset Formula $\{C/x\}$ +\end_inset + + se hace sobre una constante +\begin_inset Formula $C$ +\end_inset + + nueva, y entonces se debe añadir a las listas de todas las expresiones + de +\begin_inset Formula $\gamma$ +\end_inset + +-reglas dicha constante. +\end_layout + +\begin_layout Standard +Al aplicar estas reglas, se debe indicar, por ejemplo: +\begin_inset Formula $\gamma:\forall x;\{C/x\};C\text{ nueva}$ +\end_inset + + (la última parte se incluye siempre en las +\begin_inset Formula $\delta$ +\end_inset + +-reglas). + Las +\begin_inset Formula $\delta$ +\end_inset + +-reglas se aplican después de las +\begin_inset Formula $\beta$ +\end_inset + +-reglas y antes de las +\begin_inset Formula $\gamma$ +\end_inset + +-reglas, y si se llega a un bucle por una rama, se razona que el tableaux + es abierto. +\end_layout + +\begin_layout Standard +Si el tableaux es cerrado (si todas las hojas están cerradas), llegamos + a una contradicción. + Sin embargo, si el tableaux es abierto, no sabemos que sea satisfacible + (salvo si todos los predicados son de aridad 1 o la identidad). + No obstante, los nodos abiertos pueden servir como ejemplos de interpretaciones + en las que la oración es satisfacible. +\end_layout + +\begin_layout Section +Grafos semánticos +\end_layout + +\begin_layout Standard +Son iguales que en L0, pero en los cuantificadores, el nombre de la variable + se incluye en el nombre del propio nodo junto con el cuantificador. + Además, debajo de cada predicado (que se escribe completo), se puede indicar + el f.b.f. + de términos, que consiste en añadir un nodo hijo por cada término. + Si el término es una función, se indica simplemente el nombre de la función + y sus parámetros se escriben como nodos hijo. +\end_layout + +\begin_layout Section +Deducción natural +\end_layout + +\begin_layout Standard +Se añaden reglas de deducción natural: +\end_layout + +\begin_layout Itemize +\begin_inset Formula $E_{\forall}:\frac{\vdash\forall x\alpha[x]}{\vdash\alpha[C]}$ +\end_inset + +. + +\begin_inset Formula $C$ +\end_inset + + es una constante cualquiera. + Se debe indicar la sustitución +\begin_inset Formula $\{C/x\}$ +\end_inset + + y, en su caso, si +\begin_inset Formula $C$ +\end_inset + + es nueva o +\begin_inset Quotes cld +\end_inset + +arbitraria +\begin_inset Quotes crd +\end_inset + +. +\end_layout + +\begin_layout Itemize +\begin_inset Formula $I_{\forall}:\frac{\vdash\alpha[C]}{\vdash\forall x\alpha[x]}$ +\end_inset + +. + +\begin_inset Formula $C$ +\end_inset + + debe ser +\begin_inset Quotes cld +\end_inset + +arbitraria +\begin_inset Quotes crd +\end_inset + +, es decir, no distinguible de cualquier otro individuo por suposiciones, + derivaciones o premisas anteriores. + Puede ser obtenida nueva con +\begin_inset Formula $E_{\forall}$ +\end_inset + +. +\end_layout + +\begin_layout Itemize +\begin_inset Formula $E_{\exists}:\frac{\vdash\exists x\alpha[x]\vdash(\alpha[C]\vdash\beta)}{\vdash\beta}$ +\end_inset + +. + No se debe hacer ninguna suposición sobre +\begin_inset Formula $C$ +\end_inset + +, y +\begin_inset Formula $\beta$ +\end_inset + + no puede depender de +\begin_inset Formula $C$ +\end_inset + +. +\end_layout + +\begin_layout Itemize +\begin_inset Formula $I_{\exists}:\frac{\vdash\alpha[C]}{\vdash\exists x\alpha[x]}$ +\end_inset + +. + Se pueden cambiar todas las apariciones de +\begin_inset Formula $C$ +\end_inset + + o solo algunas. +\end_layout + +\end_body +\end_document diff --git a/fli/n7.lyx b/fli/n7.lyx new file mode 100644 index 0000000..b05b04e --- /dev/null +++ b/fli/n7.lyx @@ -0,0 +1,609 @@ +#LyX 2.3 created this file. For more info see http://www.lyx.org/ +\lyxformat 544 +\begin_document +\begin_header +\save_transient_properties true +\origin unavailable +\textclass book +\use_default_options true +\maintain_unincluded_children false +\language spanish +\language_package default +\inputencoding auto +\fontencoding global +\font_roman "default" "default" +\font_sans "default" "default" +\font_typewriter "default" "default" +\font_math "auto" "auto" +\font_default_family default +\use_non_tex_fonts false +\font_sc false +\font_osf false +\font_sf_scale 100 100 +\font_tt_scale 100 100 +\use_microtype false +\use_dash_ligatures true +\graphics default +\default_output_format default +\output_sync 0 +\bibtex_command default +\index_command default +\paperfontsize default +\spacing single +\use_hyperref false +\papersize default +\use_geometry false +\use_package amsmath 1 +\use_package amssymb 1 +\use_package cancel 1 +\use_package esint 1 +\use_package mathdots 1 +\use_package mathtools 1 +\use_package mhchem 1 +\use_package stackrel 1 +\use_package stmaryrd 1 +\use_package undertilde 1 +\cite_engine basic +\cite_engine_type default +\biblio_style plain +\use_bibtopic false +\use_indices false +\paperorientation portrait +\suppress_date false +\justification true +\use_refstyle 1 +\use_minted 0 +\index Index +\shortcut idx +\color #008000 +\end_index +\secnumdepth 3 +\tocdepth 3 +\paragraph_separation indent +\paragraph_indentation default +\is_math_indent 0 +\math_numbering_side default +\quotes_style swiss +\dynamic_quotes 0 +\papercolumns 1 +\papersides 1 +\paperpagestyle default +\tracking_changes false +\output_changes false +\html_math_output 0 +\html_css_as_file 0 +\html_be_strict false +\end_header + +\begin_body + +\begin_layout Standard +Un +\series bold +sistema deductivo +\series default + es un conjunto de axiomas y reglas de inferencia sintácticas ( +\begin_inset Formula $\vdash$ +\end_inset + +). + Una +\series bold +demostración +\series default + o +\series bold +prueba formal +\series default + es una secuencia de conjuntos de fórmulas en las que cada fórmula es un + axioma o puede obtenerse del conjunto anterior mediante una regla de inferencia. + Cada elemento +\begin_inset Formula $\alpha$ +\end_inset + + del último conjunto de la secuencia se llama +\series bold +teorema por deducción +\series default +, y se dice que +\begin_inset Formula $\alpha$ +\end_inset + + es +\series bold +demostrable +\series default +, lo que escribimos como +\begin_inset Formula $\vdash\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Standard +Un sistema deductivo en L0 y L1 es +\series bold +sólido +\series default + si y sólo si +\begin_inset Formula $\vdash\alpha\implies\vDash\alpha$ +\end_inset + +, es decir, si cualquier conclusión +\series bold +derivable +\series default + o +\series bold +deducible +\series default +a partir de las reglas es válida, y es +\series bold +completo +\series default + cuando +\begin_inset Formula $\vDash\alpha\implies\vdash\alpha$ +\end_inset + +. + Un conjunto de reglas es +\series bold +inconsistente +\series default + si +\begin_inset Formula $\vdash\alpha\land\neg\alpha$ +\end_inset + +, y es +\series bold +consistente +\series default + si no es inconsistente. +\end_layout + +\begin_layout Standard +Dada una oración +\begin_inset Formula $\alpha$ +\end_inset + + y un conjunto de oraciones +\begin_inset Formula ${\cal F}$ +\end_inset + +, +\begin_inset Formula $\vDash\alpha$ +\end_inset + + significa que +\begin_inset Formula $\alpha$ +\end_inset + + es válida y +\begin_inset Formula ${\cal F}\vDash\alpha$ +\end_inset + + significa que +\begin_inset Formula $\alpha$ +\end_inset + + es consecuencia lógica de +\begin_inset Formula ${\cal F}$ +\end_inset + +. + Por su parte +\begin_inset Formula $\vdash\alpha$ +\end_inset + + significa que +\begin_inset Formula $\alpha$ +\end_inset + + es demostrable y +\begin_inset Formula ${\cal F}\vdash\alpha$ +\end_inset + + significa que +\begin_inset Formula $\alpha$ +\end_inset + + es deducible de +\begin_inset Formula ${\cal F}$ +\end_inset + +, y representa una +\series bold +deducción +\series default + o +\series bold +razonamiento +\series default +, donde +\begin_inset Formula $\alpha$ +\end_inset + + es la conclusión o +\series bold +derivación +\series default + y las +\begin_inset Formula $\psi\in{\cal F}$ +\end_inset + + son las premisas, las fórmulas usadas para llegar a +\begin_inset Formula $\alpha$ +\end_inset + +. + +\end_layout + +\begin_layout Standard +Decimos que un conjunto de oraciones +\begin_inset Formula ${\cal T}$ +\end_inset + + es una +\series bold +teoría +\series default + si +\begin_inset Formula $\forall\alpha({\cal T}\vDash\alpha\implies\alpha\in{\cal T})$ +\end_inset + +, y entonces cada +\begin_inset Formula $\alpha\in{\cal T}$ +\end_inset + + es un +\series bold +teorema +\series default +. + Una teoría es +\series bold +axiomatizable +\series default + si existe un subconjunto +\begin_inset Formula ${\cal F}$ +\end_inset + + tal que +\begin_inset Formula ${\cal T}=\{\alpha|{\cal F}\vDash\alpha\}$ +\end_inset + +, y cada +\begin_inset Formula $\alpha\in{\cal F}$ +\end_inset + + es un +\series bold +axioma +\series default +, y es +\series bold +contradictoria +\series default + o +\series bold +inconsistente +\series default + cuando +\begin_inset Formula ${\cal T}\vDash\alpha$ +\end_inset + + y +\begin_inset Formula ${\cal T}\vDash\neg\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Standard +Una teoría es +\series bold +decidible +\series default + si se puede determinar la consistencia o inconsistencia de una fórmula + mediante un algoritmo; +\series bold +semidecidible +\series default + si hay fórmulas cuya inconsistencia no puede ser probada algorítmicamente, + e +\series bold +indecidible +\series default + si no es posible crear un algoritmo que determine la consistencia o inconsisten +cia de una fórmula. +\end_layout + +\begin_layout Standard + +\series bold +Hilbert +\series default + opinaba que todo sistema fundamental matemático debía ser consistente, + completo y decidible, pero Kurt +\series bold + Gödel +\series default + demostró que ningún sistema capaz de representar los números naturales + puede ser a la vez consistente y completo, y que la consistencia no puede + probarse con los propios axiomas del sistema, por lo que habrá verdades + que no se pueden demostrar. + Alan +\series bold +Turing +\series default +, por su parte, demostró que solo sistemas muy restrictivos son decidibles. +\end_layout + +\begin_layout Standard +Un sistema deductivo cumple el +\series bold +teorema de la deducción +\series default + si verifica que, dado el conjunto +\begin_inset Formula ${\cal F}$ +\end_inset + + y las fórmulas +\begin_inset Formula $\alpha$ +\end_inset + + y +\begin_inset Formula $\beta$ +\end_inset + +, +\begin_inset Formula ${\cal F}\cup\{\alpha\}\vdash\beta\iff{\cal F}\vdash\alpha\rightarrow\beta$ +\end_inset + +. + Así, +\begin_inset Formula ${\cal F}\cup\{\alpha_{1},\dots,\alpha_{n}\}\vdash\beta\iff{\cal F}\cup\{\alpha_{1},\dots,\alpha_{n-1}\}\vdash\alpha_{n}\rightarrow\beta\iff\dots\iff{\cal F}\vdash\alpha_{1}\rightarrow(\alpha_{2}\rightarrow\cdots(\alpha_{n}\rightarrow\beta)\cdots)$ +\end_inset + +. + Este teorema simplifica mucho las demostraciones, si bien no se probó su + corrección hasta 1930. + No todos los sistemas cumplen en teorema de la deducción, si bien el Teorema + de la Deducción Semántica ( +\begin_inset Formula ${\cal F}\cup\{a\}\vDash\beta\iff{\cal F}\vDash\alpha\rightarrow\beta$ +\end_inset + +) se cumple siempre. + Decimos que +\begin_inset Formula ${\cal F}$ +\end_inset + + es +\series bold +sintácticamente completo +\series default + si para todo +\begin_inset Formula $\alpha$ +\end_inset + +, +\begin_inset Formula ${\cal F}\vdash\alpha$ +\end_inset + + o +\begin_inset Formula ${\cal F}\vdash\neg\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Standard +Un +\series bold +razonamiento deductivo +\series default + es el que parte de unas hipótesis básicas para obtener unas consecuencias + ( +\begin_inset Formula $\alpha\vDash\beta$ +\end_inset + +). + Normalmente parte de premisas sobre aspectos generales para concluir aspectos + particulares. + La relación entre premisas y conclusión es de implicación ( +\begin_inset Formula $\alpha\vDash\beta\iff\vDash\alpha\rightarrow\beta$ +\end_inset + +). + Algunos tipos de +\series bold +demostración +\series default + deductiva (de +\begin_inset Formula $\vDash\alpha\rightarrow\beta$ +\end_inset + +): +\end_layout + +\begin_layout Itemize + +\series bold +Vacía +\series default + de +\begin_inset Formula $\alpha\rightarrow\beta$ +\end_inset + +: +\begin_inset Formula $\forall v_{I},v(\alpha)=F$ +\end_inset + + (no se usa +\begin_inset Formula $\beta$ +\end_inset + +). +\end_layout + +\begin_layout Itemize + +\series bold +Trivial +\series default +: +\begin_inset Formula $\forall v_{I},v(\beta)=V$ +\end_inset + + (no se usa +\begin_inset Formula $\alpha$ +\end_inset + +). +\end_layout + +\begin_layout Itemize + +\series bold +Directa +\series default +: Probar que +\begin_inset Formula $\alpha\vDash\beta$ +\end_inset + + usando definiciones o teoremas ya probados, como el Modus Ponens. +\end_layout + +\begin_layout Itemize + +\series bold +Por contrarrecíproco +\series default +: +\begin_inset Formula $\alpha\rightarrow\beta\equiv\neg\beta\rightarrow\neg\alpha$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Por contradicción +\series default +: +\begin_inset Formula $\alpha\rightarrow\beta\equiv\alpha\land\neg\beta\rightarrow\gamma\land\neg\gamma$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Indirecta +\series default +: Si +\begin_inset Formula $\alpha\vDash\gamma$ +\end_inset + + y +\begin_inset Formula $\gamma\vDash\beta$ +\end_inset + + entonces +\begin_inset Formula $\alpha\vDash\beta$ +\end_inset + +. +\end_layout + +\begin_layout Standard +La +\series bold +refutación por contraejemplo +\series default + consiste en buscar +\begin_inset Formula $a$ +\end_inset + + tal que +\begin_inset Formula $v(\alpha[a]\rightarrow\beta[a])=F$ +\end_inset + +. +\end_layout + +\begin_layout Standard +Un +\series bold +razonamiento inductivo +\series default + consiste en obtener reglas generales a partir de casos particulares. + Para ello se observan, registran y analizan hechos y se formulan leyes + universales a modo de hipótesis o conjeturas, tras lo cual se diseñan experimen +tos para ver que estas leyes se cumplen. +\end_layout + +\begin_layout Standard +La +\series bold +inducción matemática +\series default +, sin embargo, se puede probar de forma deductiva, si bien esto requiere + lógica de segundo orden. + En +\begin_inset Formula $\mathbb{N}$ +\end_inset + +, para un +\begin_inset Formula $n_{0}\in\mathbb{N}$ +\end_inset + +, tenemos: +\end_layout + +\begin_layout Itemize + +\series bold +Principio de inducción débil +\series default +: +\begin_inset Formula $\{P(n_{0})\}\cup\bigcup_{n\geq n_{0}}\{P(n)\rightarrow P(n+1)\}\vDash\forall n\geq n_{0},P(n)$ +\end_inset + +. +\end_layout + +\begin_layout Itemize + +\series bold +Principio de inducción fuerte +\series default +: +\begin_inset Formula $\{P(n_{0})\}\cup\bigcup_{n\geq n_{0}}\{P(n_{0})\land\dots\land P(n)\rightarrow P(n+1)\}\vDash\forall n\geq n_{0},P(n)$ +\end_inset + +. +\end_layout + +\begin_layout Standard +El +\series bold +principio de inducción estructural +\series default + para +\series bold +demostración por recursión +\series default + es una generalización de la inducción y afirma que, dado un conjunto de + elementos definido por recursión con una serie de casos base y reglas de + recursión sobre estos, si una propiedad se cumple para cada caso base, + y si en cada regla de recursión si la propiedad se cumple para los parámetros + de entrada también se cumple para el elemento resultante de aplicarla, + entonces esta propiedad la cumplen todos los elementos del conjunto. +\end_layout + +\end_body +\end_document diff --git a/logic/n.lyx b/logic/n.lyx deleted file mode 100644 index 57fe1dd..0000000 --- a/logic/n.lyx +++ /dev/null @@ -1,253 +0,0 @@ -#LyX 2.3 created this file. For more info see http://www.lyx.org/ -\lyxformat 544 -\begin_document -\begin_header -\save_transient_properties true -\origin unavailable -\textclass book -\use_default_options true -\maintain_unincluded_children false -\language spanish -\language_package default -\inputencoding auto -\fontencoding global -\font_roman "default" "default" -\font_sans "default" "default" -\font_typewriter "default" "default" -\font_math "auto" "auto" -\font_default_family default -\use_non_tex_fonts false -\font_sc false -\font_osf false -\font_sf_scale 100 100 -\font_tt_scale 100 100 -\use_microtype false -\use_dash_ligatures true -\graphics default -\default_output_format default -\output_sync 0 -\bibtex_command default -\index_command default -\paperfontsize default -\spacing single -\use_hyperref false -\papersize a5paper -\use_geometry true -\use_package amsmath 1 -\use_package amssymb 1 -\use_package cancel 1 -\use_package esint 1 -\use_package mathdots 1 -\use_package mathtools 1 -\use_package mhchem 1 -\use_package stackrel 1 -\use_package stmaryrd 1 -\use_package undertilde 1 -\cite_engine basic -\cite_engine_type default -\biblio_style plain -\use_bibtopic false -\use_indices false -\paperorientation portrait -\suppress_date false -\justification true -\use_refstyle 1 -\use_minted 0 -\index Index -\shortcut idx -\color #008000 -\end_index -\leftmargin 0.2cm -\topmargin 0.7cm -\rightmargin 0.2cm -\bottommargin 0.7cm -\secnumdepth 3 -\tocdepth 3 -\paragraph_separation indent -\paragraph_indentation default -\is_math_indent 0 -\math_numbering_side default -\quotes_style swiss -\dynamic_quotes 0 -\papercolumns 1 -\papersides 1 -\paperpagestyle empty -\tracking_changes false -\output_changes false -\html_math_output 0 -\html_css_as_file 0 -\html_be_strict false -\end_header - -\begin_body - -\begin_layout Title -Fundamentos Lógicos de la Informática -\end_layout - -\begin_layout Date -\begin_inset Note Note -status open - -\begin_layout Plain Layout - -\end_layout - -\end_inset - - -\end_layout - -\begin_layout Standard -\begin_inset ERT -status open - -\begin_layout Plain Layout - - -\backslash -def -\backslash -cryear{2017} -\end_layout - -\end_inset - - -\end_layout - -\begin_layout Standard -\begin_inset CommandInset include -LatexCommand input -filename "../license.lyx" - -\end_inset - - -\end_layout - -\begin_layout Standard -Bibliografía: -\end_layout - -\begin_layout Itemize -Diapositivas de Fundamentos Lógicos de la Informática, Departamento de Ingenierí -a de al Información y las Comunicaciones (nota: la errata es de ellos), - Facultad de Informática, Universidad de Murcia. -\end_layout - -\begin_layout Itemize -Wikipedia, la enciclopedia libre ( -\begin_inset Flex URL -status open - -\begin_layout Plain Layout - -https://es.wikipedia.org/ -\end_layout - -\end_inset - -). -\end_layout - -\begin_layout Chapter -Lógica -\end_layout - -\begin_layout Standard -\begin_inset CommandInset include -LatexCommand input -filename "n1.lyx" - -\end_inset - - -\end_layout - -\begin_layout Chapter -Lógica proposicional -\end_layout - -\begin_layout Standard -\begin_inset CommandInset include -LatexCommand input -filename "n2.lyx" - -\end_inset - - -\end_layout - -\begin_layout Chapter -Problema SAT -\end_layout - -\begin_layout Standard -\begin_inset CommandInset include -LatexCommand input -filename "n3.lyx" - -\end_inset - - -\end_layout - -\begin_layout Chapter -Deducción natural -\end_layout - -\begin_layout Standard -\begin_inset CommandInset include -LatexCommand input -filename "n4.lyx" - -\end_inset - - -\end_layout - -\begin_layout Chapter -Lógica categórica -\end_layout - -\begin_layout Standard -\begin_inset CommandInset include -LatexCommand input -filename "n5.lyx" - -\end_inset - - -\end_layout - -\begin_layout Chapter -Lógica de predicados de primer orden -\end_layout - -\begin_layout Standard -\begin_inset CommandInset include -LatexCommand input -filename "n6.lyx" - -\end_inset - - -\end_layout - -\begin_layout Chapter -Sistemas deductivos, razonamientos y deducciones -\end_layout - -\begin_layout Standard -\begin_inset CommandInset include -LatexCommand input -filename "n7.lyx" - -\end_inset - - -\end_layout - -\end_body -\end_document diff --git a/logic/n1.lyx b/logic/n1.lyx deleted file mode 100644 index 166b2b3..0000000 --- a/logic/n1.lyx +++ /dev/null @@ -1,346 +0,0 @@ -#LyX 2.3 created this file. For more info see http://www.lyx.org/ -\lyxformat 544 -\begin_document -\begin_header -\save_transient_properties true -\origin unavailable -\textclass book -\use_default_options true -\maintain_unincluded_children false -\language spanish -\language_package default -\inputencoding auto -\fontencoding global -\font_roman "default" "default" -\font_sans "default" "default" -\font_typewriter "default" "default" -\font_math "auto" "auto" -\font_default_family default -\use_non_tex_fonts false -\font_sc false -\font_osf false -\font_sf_scale 100 100 -\font_tt_scale 100 100 -\use_microtype false -\use_dash_ligatures true -\graphics default -\default_output_format default -\output_sync 0 -\bibtex_command default -\index_command default -\paperfontsize default -\spacing single -\use_hyperref false -\papersize default -\use_geometry false -\use_package amsmath 1 -\use_package amssymb 1 -\use_package cancel 1 -\use_package esint 1 -\use_package mathdots 1 -\use_package mathtools 1 -\use_package mhchem 1 -\use_package stackrel 1 -\use_package stmaryrd 1 -\use_package undertilde 1 -\cite_engine basic -\cite_engine_type default -\biblio_style plain -\use_bibtopic false -\use_indices false -\paperorientation portrait -\suppress_date false -\justification true -\use_refstyle 1 -\use_minted 0 -\index Index -\shortcut idx -\color #008000 -\end_index -\secnumdepth 3 -\tocdepth 3 -\paragraph_separation indent -\paragraph_indentation default -\is_math_indent 0 -\math_numbering_side default -\quotes_style swiss -\dynamic_quotes 0 -\papercolumns 1 -\papersides 1 -\paperpagestyle default -\tracking_changes false -\output_changes false -\html_math_output 0 -\html_css_as_file 0 -\html_be_strict false -\end_header - -\begin_body - -\begin_layout Standard -La lógica estudia las oraciones y los razonamientos, y existen tantas como - tipos de oraciones y razonamientos. - En informática, es la base de la programación, representa el conocimiento - en inteligencia artificial, sirve para demostraciones de resultados teóricos - y diseño de circuitos lógicos y define los problemas NP-completos (SAT). - Existen distintas lógicas, como las lógicas clásicas (proposicional, categórica -, de primer orden...) y la lógica difusa. -\end_layout - -\begin_layout Section -Oraciones -\end_layout - -\begin_layout Standard -Dentro de una misma lógica, una oración lógica es una oración del lenguaje - natural que cumpla ciertas condiciones. - En las lógicas clásicas, es aquella que es -\series bold -enunciativa -\series default - y cumple la -\series bold -ley del tercero excluido -\series default - (solo puede ser verdadera [ -\begin_inset Formula $V$ -\end_inset - -] o falsa [ -\begin_inset Formula $F$ -\end_inset - -]) y la -\series bold -ley de no contradicción -\series default - (no puede ser -\begin_inset Formula $V$ -\end_inset - - y -\begin_inset Formula $F$ -\end_inset - - a la vez). - Estas pueden ser -\series bold -simples -\series default - ( -\series bold -atómicas -\series default -) o -\series bold -compuestas -\series default - ( -\series bold -moleculares -\series default -), dependiendo de si tienen uno o más predicados. -\end_layout - -\begin_layout Section -Razonamientos -\end_layout - -\begin_layout Standard -Un razonamiento es una estructura que enlaza oraciones, de las cuales una - es la -\series bold -conclusión -\series default - de otras ( -\series bold -premisas -\series default -) y todas (salvo ella misma) proporcionan evidencias para justificarla. - Así, un razonamiento está formado por -\series bold -axiomas -\series default - o -\series bold -premisas -\series default -; -\series bold -conclusiones -\series default - o -\series bold -teoremas -\series default -, y una -\series bold -demostración -\series default -. - Existen dos tipos de razonamiento: -\end_layout - -\begin_layout Itemize - -\series bold -Deductivo: -\series default - Se basa en la implicación. -\end_layout - -\begin_layout Itemize - -\series bold -Inductivo: -\series default - Parte de casos y llega a una conclusión general. - Sólo es válido si se consideran todos los casos; de lo contrario la conclusión - es probablemente, pero no necesariamente, cierta. -\end_layout - -\begin_layout Standard -Un razonamiento es válido si la conclusión es necesariamente cierta cuando - lo son las premisas, y se escribe como -\begin_inset Formula $\underset{\text{Premisas}}{\{\alpha_{1},\alpha_{2},\dots,\alpha_{n}\}}\vDash\underset{\text{Conclusión}}{\beta}$ -\end_inset - -. - Para representarlo: -\end_layout - -\begin_layout Itemize - -\series bold -Representación gráfica: -\series default - -\begin_inset Formula -\[ -\begin{array}{ccccc} -P_{1} & \land & P_{2}\\ -\hline & \downarrow\\ - & C_{1} & & \land & P_{3}\\ -\hline & & & \downarrow\\ - & & & C_{2} -\end{array} -\] - -\end_inset - - -\end_layout - -\begin_layout Itemize - -\series bold -Representación estándar: -\begin_inset Formula -\[ -\begin{array}{ccc} - & P_{1}\\ - & P_{2}\\ -\hline \therefore & C_{1} & P_{1}\text{ y }P_{2}\\ - & P_{3}\\ -\hline \therefore & C_{2} & C_{1}\text{ y }P_{3} -\end{array} -\] - -\end_inset - - -\end_layout - -\begin_layout Section -Tipos de definiciones -\end_layout - -\begin_layout Itemize - -\series bold -Extensiva -\series default - o -\series bold -extensional: -\series default - Lista de elementos que cumplen la condición. -\end_layout - -\begin_layout Itemize - -\series bold -Comprensiva -\series default - o -\series bold -intensional: -\series default - Lista de propiedades necesarias. -\end_layout - -\begin_layout Itemize - -\series bold -Recursiva: -\series default - Formada por una -\series bold -regla base -\series default -, que define casos concretos, y una -\series bold -regla recursiva -\series default -, que define todos los demás casos a partir de casos ya conocidos mediante - una relación. - También puede contener una -\series bold -regla de exclusión -\series default -. -\end_layout - -\begin_layout Section -Lenguajes formales -\end_layout - -\begin_layout Standard -El lenguaje natural es ambiguo, y suele ser vago, paradójico, complicado... - Por tanto, en ciencia es imprescindible un lenguaje formal para obtener - rigor. - Un lenguaje formal consta de un conjunto de símbolos ( -\series bold -alfabeto -\series default - o -\series bold -vocabulario -\series default -) y una definición recursiva para conectarlos ( -\series bold -gramática -\series default - o -\series bold -sintaxis -\series default -), y es el conjunto de todas las fórmulas bien formadas (f.b.f.) obtenidas - a partir de estas. - En la práctica, necesitamos un sistema de codificación (formalización) - y de interpretación. -\end_layout - -\begin_layout Section -Formalización e interpretación -\end_layout - -\begin_layout Standard -Formalizar es obtener una oración o f.b.f. - en lenguaje formal a partir del lenguaje natural, mientras que interpretar - es entender una f.b.f. - expresándola en lenguaje natural. -\end_layout - -\end_body -\end_document diff --git a/logic/n2.lyx b/logic/n2.lyx deleted file mode 100644 index 93478b7..0000000 --- a/logic/n2.lyx +++ /dev/null @@ -1,1518 +0,0 @@ -#LyX 2.3 created this file. For more info see http://www.lyx.org/ -\lyxformat 544 -\begin_document -\begin_header -\save_transient_properties true -\origin unavailable -\textclass book -\use_default_options true -\maintain_unincluded_children false -\language spanish -\language_package default -\inputencoding auto -\fontencoding global -\font_roman "default" "default" -\font_sans "default" "default" -\font_typewriter "default" "default" -\font_math "auto" "auto" -\font_default_family default -\use_non_tex_fonts false -\font_sc false -\font_osf false -\font_sf_scale 100 100 -\font_tt_scale 100 100 -\use_microtype false -\use_dash_ligatures true -\graphics default -\default_output_format default -\output_sync 0 -\bibtex_command default -\index_command default -\paperfontsize default -\spacing single -\use_hyperref false -\papersize default -\use_geometry false -\use_package amsmath 1 -\use_package amssymb 1 -\use_package cancel 1 -\use_package esint 1 -\use_package mathdots 1 -\use_package mathtools 1 -\use_package mhchem 1 -\use_package stackrel 1 -\use_package stmaryrd 1 -\use_package undertilde 1 -\cite_engine basic -\cite_engine_type default -\biblio_style plain -\use_bibtopic false -\use_indices false -\paperorientation portrait -\suppress_date false -\justification true -\use_refstyle 1 -\use_minted 0 -\index Index -\shortcut idx -\color #008000 -\end_index -\secnumdepth 3 -\tocdepth 3 -\paragraph_separation indent -\paragraph_indentation default -\is_math_indent 0 -\math_numbering_side default -\quotes_style swiss -\dynamic_quotes 0 -\papercolumns 1 -\papersides 1 -\paperpagestyle default -\tracking_changes false -\output_changes false -\html_math_output 0 -\html_css_as_file 0 -\html_be_strict false -\end_header - -\begin_body - -\begin_layout Standard -Las oraciones lógicas en lógica proposicional ( -\series bold -L0 -\series default -) se llaman -\series bold -proposiciones -\series default -. - Las proposiciones atómicas, también llamadas -\series bold -sentencias -\series default - o -\series bold -átomos -\series default -, se agrupan mediante -\series bold -operadores lógicos -\series default - para formar oraciones compuestas. -\end_layout - -\begin_layout Section -Sintaxis -\end_layout - -\begin_layout Itemize - -\series bold -Constantes: -\series default - Verdadero ( -\begin_inset Formula $V$ -\end_inset - -) o falso ( -\begin_inset Formula $F$ -\end_inset - -). - -\begin_inset Formula $\mathbb{B}=\{V,F\}$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Sentencias: -\series default - Se representan por un conjunto de letras latinas. - El conjunto de todos se denota por -\begin_inset Formula ${\cal P}$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Operadores lógicos: -\series default - Negación ( -\begin_inset Formula $\neg$ -\end_inset - -) y conectivos. - Los conectivos son: conjunción ( -\begin_inset Formula $\land$ -\end_inset - -), disyunción ( -\begin_inset Formula $\lor$ -\end_inset - -), implicación ( -\begin_inset Formula $\rightarrow$ -\end_inset - -) y doble implicación ( -\begin_inset Formula $\leftrightarrow$ -\end_inset - -). -\end_layout - -\begin_layout Itemize - -\series bold -Paréntesis -\series default - o corchetes, para agrupar expresiones. -\end_layout - -\begin_layout Standard -Definición recursiva de una f.b.f.: -\end_layout - -\begin_layout Itemize - -\series bold -Forma básica: -\series default - Todo átomo es una f.b.f. -\end_layout - -\begin_layout Itemize - -\series bold -Forma recursiva: -\series default - Si -\begin_inset Formula $\alpha$ -\end_inset - - y -\begin_inset Formula $\beta$ -\end_inset - - son f.b.f., también lo son -\begin_inset Formula $\neg\alpha$ -\end_inset - -, -\begin_inset Formula $(\alpha\land\beta)$ -\end_inset - -, -\begin_inset Formula $(\alpha\lor\beta)$ -\end_inset - -, -\begin_inset Formula $(\alpha\rightarrow\beta)$ -\end_inset - - y -\begin_inset Formula $(\alpha\leftrightarrow\beta)$ -\end_inset - -. - La presencia o ausencia de paréntesis es importante. -\end_layout - -\begin_layout Standard -En la práctica, podemos eliminar paréntesis según estas reglas: -\end_layout - -\begin_layout Itemize -Se pueden eliminar los paréntesis exteriores. -\end_layout - -\begin_layout Itemize - -\series bold -Prioridad: -\series default - De mayor a menor: -\begin_inset Formula $\neg$ -\end_inset - -, ( -\begin_inset Formula $\land$ -\end_inset - -, -\begin_inset Formula $\lor$ -\end_inset - -), ( -\begin_inset Formula $\rightarrow$ -\end_inset - -, -\begin_inset Formula $\leftrightarrow$ -\end_inset - -). -\end_layout - -\begin_layout Itemize - -\series bold -Asociatividad: -\series default - A igual prioridad de operadores, se asocia por la izquierda. -\end_layout - -\begin_layout Standard -También podemos añadir paréntesis a cualquier expresión que no sea una negación. -\end_layout - -\begin_layout Section -Formalización -\end_layout - -\begin_layout Itemize -Los átomos corresponden a oraciones enunciativas afirmativas, en forma presente - y con sujeto (salvo verbos impersonales). -\end_layout - -\begin_layout Itemize -\begin_inset Formula $\neg\alpha$ -\end_inset - -: No -\begin_inset Formula $\alpha$ -\end_inset - -, no es el caso de -\begin_inset Formula $\alpha$ -\end_inset - -, no es cierto que -\begin_inset Formula $\alpha$ -\end_inset - -, es falso que -\begin_inset Formula $\alpha$ -\end_inset - -, no sucede que -\begin_inset Formula $\alpha$ -\end_inset - -, la negación de -\begin_inset Formula $\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Itemize -\begin_inset Formula $\alpha\land\beta$ -\end_inset - -: -\begin_inset Formula $\alpha$ -\end_inset - - y -\begin_inset Formula $\beta$ -\end_inset - - (pero, aunque, además, sin embargo, también, a la vez, aún, no obstante). -\end_layout - -\begin_layout Itemize -\begin_inset Formula $\alpha\lor\beta$ -\end_inset - -: O -\begin_inset Formula $\alpha$ -\end_inset - - o -\begin_inset Formula $\beta$ -\end_inset - -; ya -\begin_inset Formula $\alpha$ -\end_inset - -, ya -\begin_inset Formula $\beta$ -\end_inset - -, ya ambas. -\end_layout - -\begin_layout Itemize -\begin_inset Formula $\alpha\rightarrow\beta$ -\end_inset - -: Si -\begin_inset Formula $\alpha$ -\end_inset - - -\begin_inset Formula $\beta$ -\end_inset - -, si -\begin_inset Formula $\alpha$ -\end_inset - - entonces -\begin_inset Formula $\beta$ -\end_inset - -, -\begin_inset Formula $\alpha$ -\end_inset - - solo si -\begin_inset Formula $\beta$ -\end_inset - -, solo -\begin_inset Formula $\alpha$ -\end_inset - - si -\begin_inset Formula $\beta$ -\end_inset - -, es suficiente -\begin_inset Formula $\alpha$ -\end_inset - - para que -\begin_inset Formula $\beta$ -\end_inset - -, siempre que -\begin_inset Formula $\alpha$ -\end_inset - - entonces -\begin_inset Formula $\beta$ -\end_inset - -, no -\begin_inset Formula $\alpha$ -\end_inset - - a menos que -\begin_inset Formula $\beta$ -\end_inset - -, es necesario -\begin_inset Formula $\beta$ -\end_inset - - para que -\begin_inset Formula $\alpha$ -\end_inset - -, a no ser que -\begin_inset Formula $\beta$ -\end_inset - - no -\begin_inset Formula $\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Itemize -\begin_inset Formula $\alpha\leftrightarrow\beta$ -\end_inset - -: -\begin_inset Formula $\alpha$ -\end_inset - - si y sólo si -\begin_inset Formula $\beta$ -\end_inset - -, -\begin_inset Formula $\alpha$ -\end_inset - - equivale a -\begin_inset Formula $\beta$ -\end_inset - -, -\begin_inset Formula $\alpha$ -\end_inset - - cuando y sólo cuando -\begin_inset Formula $\beta$ -\end_inset - -, -\begin_inset Formula $\alpha$ -\end_inset - - cuando únicamente -\begin_inset Formula $\beta$ -\end_inset - - , -\begin_inset Formula $\alpha$ -\end_inset - - es condición suficiente y necesaria para que -\begin_inset Formula $\beta$ -\end_inset - -. -\end_layout - -\begin_layout Section -Interpretación -\end_layout - -\begin_layout Standard -Procedimiento que traduce las fórmulas -\series bold -atómicas -\series default - a oraciones naturales. - Una -\series bold -asignación -\series default - -\begin_inset Formula $v_{I}$ -\end_inset - - es el procedimiento que establece un valor de verdad a una fórmula atómica - según una interpretación -\begin_inset Formula $I$ -\end_inset - -. - En L0 no se suele hacer distinción, y hace referencia a una función -\begin_inset Formula $v_{I}:{\cal P_{\alpha}}\rightarrow\mathbb{B}$ -\end_inset - - tal que -\begin_inset Formula $V\mapsto V$ -\end_inset - - y -\begin_inset Formula $F\mapsto F$ -\end_inset - -. -\end_layout - -\begin_layout Standard -La -\series bold -evaluación -\series default - es la obtención del valor de verdad de una oración -\begin_inset Formula $\alpha$ -\end_inset - -. - Decimos -\begin_inset Formula $V(\alpha)=V$ -\end_inset - - o -\begin_inset Formula $V(\alpha)=F$ -\end_inset - -, según corresponda. -\end_layout - -\begin_layout Itemize - -\series bold -Regla base: -\series default - Si -\begin_inset Formula $\alpha\in{\cal P}$ -\end_inset - -, entonces -\begin_inset Formula $V(\alpha)=v_{I}(\alpha)$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Regla recursiva: -\series default - -\begin_inset Formula -\begin{eqnarray*} -V(\neg\alpha) & = & \begin{cases} -V & \text{si }V(\alpha)=F\\ -F & \text{si }V(\alpha)=V -\end{cases}\\ -V(\alpha\land\beta) & = & \begin{cases} -V & \text{si }V(\alpha)=V\text{ y }V(\beta)=V\\ -F & \text{en otro caso} -\end{cases}\\ -V(\alpha\lor\beta) & = & \begin{cases} -F & \text{si }V(\alpha)=F\text{ y }V(\beta)=F\\ -V & \text{en otro caso} -\end{cases}\\ -V(\alpha\rightarrow\beta) & = & \begin{cases} -F & \text{si }V(\alpha)=V\text{ y }V(\beta)=F\\ -V & \text{en otro caso} -\end{cases}\\ -V(\alpha\leftrightarrow\beta) & = & \begin{cases} -V & \text{si }V(\alpha)=V(\beta)\\ -F & \text{en otro caso} -\end{cases} -\end{eqnarray*} - -\end_inset - - -\end_layout - -\begin_layout Section -Grafos semánticos -\end_layout - -\begin_layout Standard -Un grafo semántico es un árbol que representa una f.b.f. - El nodo principal contiene el operador principal (o el único átomo). - De cada conectivo parten dos ramas (o una si es -\begin_inset Formula $\neg$ -\end_inset - -) con las subfórmulas que conecta, y los átomos son hojas. -\end_layout - -\begin_layout Section -Decidibilidad -\end_layout - -\begin_layout Standard -Una oración puede ser: -\end_layout - -\begin_layout Itemize - -\series bold -Satisfacible -\series default - si -\begin_inset Formula $V(\alpha)=V$ -\end_inset - - en alguna interpretación. -\end_layout - -\begin_layout Itemize - -\series bold -Falseable -\series default - si -\begin_inset Formula $V(\alpha)=F$ -\end_inset - - en alguna interpretación. -\end_layout - -\begin_layout Itemize - -\series bold -Contingente -\series default - o -\series bold -contingencia -\series default - si es a la vez satisfacible y falseable. -\end_layout - -\begin_layout Itemize - -\series bold -Tautológica -\series default -, -\series bold -válida -\series default - o -\series bold -tautología -\series default - si -\begin_inset Formula $V(\alpha)=V$ -\end_inset - - en todas las interpretaciones. - Escribimos -\begin_inset Formula $\vDash\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Insatisfacible -\series default - o -\series bold -contradicción -\series default - si -\begin_inset Formula $V(\alpha)=F$ -\end_inset - - en todas las interpretaciones. -\end_layout - -\begin_layout Standard -El problema SAT, determinar si una oración lógica es satisfacible, es el - primer problema conocido NP-completo, y de hecho todos los problemas NP-complet -os se pueden reducir a SAT, de modo que si uno de resuelve como P, se resuelven - todos. -\end_layout - -\begin_layout Standard -Un conjunto de fórmulas -\begin_inset Formula ${\cal F}=\{\alpha_{1},\dots,\alpha_{n}\}$ -\end_inset - - es satisfacible si su conjunción lo es, y llamamos -\series bold -modelo -\series default - de -\begin_inset Formula ${\cal F}$ -\end_inset - - a cualquier interpretación en la que -\begin_inset Formula $V(\alpha_{1}\land\dots\land\alpha_{n})=V$ -\end_inset - -. - Definimos del mismo modo conjunto insatisfacible. - El conjunto -\begin_inset Formula ${\cal F}=\{\}$ -\end_inset - - es modelo en todas las interpretaciones. -\end_layout - -\begin_layout Standard -Para hallar los valores de verdad de una oración en función de la interpretación -, podemos construir una -\series bold -tabla de verdad. - -\series default - Si -\begin_inset Formula $\alpha$ -\end_inset - - tiene -\begin_inset Formula $n$ -\end_inset - - átomos y -\begin_inset Formula $m$ -\end_inset - - operadores, construimos una tabla con -\begin_inset Formula $2^{n}$ -\end_inset - - filas (más la cabecera) y -\begin_inset Formula $n+m$ -\end_inset - - columnas. - En cada fila establecemos una asignación hasta establecer todas las asignacione -s posibles y obtenemos las evaluaciones para las oraciones definidas por - cada operador, en orden de evaluación y terminando con el operador principal, - que establece el valor de verdad. - Debemos indicar el orden de evaluación. -\end_layout - -\begin_layout Standard -Otra forma es la -\series bold -propagación de literales. - -\series default - Un literal es un átomo o la negación de un átomo. - Dada una fórmula -\begin_inset Formula $\phi$ -\end_inset - -, definimos -\begin_inset Formula $\phi(p)\equiv\phi_{|V(p)=V}$ -\end_inset - - a la fórmula más simplificada que, en las interpretaciones en las que -\begin_inset Formula $V(p)=V$ -\end_inset - -, tenga los mismos valores de verdad que -\begin_inset Formula $\phi$ -\end_inset - -. - Por ejemplo, dada la oración -\begin_inset Formula $\phi\equiv(p\rightarrow q)\rightarrow(\neg p\rightarrow\neg q)$ -\end_inset - -, tendríamos que -\begin_inset Formula $\phi(p)\equiv\phi_{|V(p)=V}\equiv(V\rightarrow q)\rightarrow(\neg V\rightarrow\neg q)\equiv q\rightarrow(F\rightarrow q)\equiv q\rightarrow V\equiv V$ -\end_inset - -, mientras que -\begin_inset Formula $\phi(\neg p)\equiv\phi_{|V(\neg p)=V}\equiv\phi_{|V(p)=F}\equiv(F\rightarrow q)\rightarrow(\neg F\rightarrow\neg q)\equiv V\rightarrow(V\rightarrow\neg q)\equiv V\rightarrow\neg q\equiv\neg q$ -\end_inset - -. - En el segundo caso, tendríamos, por ejemplo, que -\begin_inset Formula $\phi(\neg p)(q)\equiv\phi(\neg p,q)\equiv\phi(\neg p)_{|V(q)=V}\equiv\neg V\equiv F$ -\end_inset - -. - En la práctica bastaría con escribir -\begin_inset Formula $\phi(\neg p,q)\equiv\neg V\equiv F$ -\end_inset - - para este último caso. -\end_layout - -\begin_layout Standard -Para comprobar los valores de verdad realizaríamos un -\series bold -árbol semántico. - -\series default - En este, la raíz sería la fórmula inicial, y de cada nodo, que contendrá - una fórmula -\begin_inset Formula $\xi$ -\end_inset - -, partirán dos ramas con -\begin_inset Formula $\xi(p)$ -\end_inset - - y -\begin_inset Formula $\xi(\neg p)$ -\end_inset - - para algún átomo -\begin_inset Formula $l$ -\end_inset - - en -\begin_inset Formula $\xi$ -\end_inset - - (normalmente el que más aparece), salvo si -\begin_inset Formula $\xi\equiv V$ -\end_inset - - o -\begin_inset Formula $\xi\equiv F$ -\end_inset - -. - A la hora de dibujarlo, la línea que une una expresión con otra derivada - se etiqueta con el literal a propagar. -\end_layout - -\begin_layout Section -Equivalencias -\end_layout - -\begin_layout Standard -Dos expresiones -\begin_inset Formula $\alpha$ -\end_inset - - y -\begin_inset Formula $\beta$ -\end_inset - - son lógicamente equivalentes si y sólo si -\begin_inset Formula $V(\alpha)=V(\beta)$ -\end_inset - - para cualquier interpretación. - Escribimos -\begin_inset Formula $\alpha\equiv\beta$ -\end_inset - -. - Así, -\begin_inset Formula $\alpha\equiv\beta\iff\vDash\alpha\leftrightarrow\beta$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Propiedades conmutativas: -\series default - -\begin_inset Formula $\alpha\land\beta\equiv\beta\land\alpha$ -\end_inset - -; -\begin_inset Formula $\alpha\lor\beta\equiv\beta\land\alpha$ -\end_inset - -; -\begin_inset Formula $\alpha\leftrightarrow\beta\equiv\beta\leftrightarrow\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Propiedades asociativas: -\series default - -\begin_inset Formula $\alpha\land(\beta\land\gamma)\equiv(\alpha\land\beta)\land\gamma$ -\end_inset - -; -\begin_inset Formula $\alpha\lor(\beta\lor\gamma)\equiv(\alpha\lor\beta)\lor\gamma$ -\end_inset - -; -\begin_inset Formula $\alpha\leftrightarrow(\beta\leftrightarrow\gamma)\equiv(\alpha\leftrightarrow\beta)\leftrightarrow\gamma$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Propiedades de De Morgan: -\series default - -\begin_inset Formula $\neg(\alpha\land\beta)\equiv\neg\alpha\lor\neg\beta$ -\end_inset - -; -\begin_inset Formula $\neg(\alpha\lor\beta)\equiv\neg\alpha\land\neg\beta$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Propiedades distributivas: -\series default - -\begin_inset Formula $\alpha\land(\beta\lor\gamma)\equiv(\alpha\land\beta)\lor(\alpha\land\gamma)$ -\end_inset - -; -\begin_inset Formula $\alpha\lor(\beta\land\gamma)\equiv(\alpha\lor\beta)\land(\alpha\lor\gamma)$ -\end_inset - -; -\begin_inset Formula $\alpha\rightarrow(\beta\lor\gamma)\equiv(\alpha\rightarrow\beta)\lor(\alpha\rightarrow\gamma)$ -\end_inset - -; -\begin_inset Formula $\alpha\rightarrow(\beta\land\gamma)\equiv(\alpha\rightarrow\beta)\land(\alpha\rightarrow\gamma)$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Propiedades de absorción: -\series default - -\begin_inset Formula $\alpha\lor(\alpha\land\beta)\equiv\alpha\land(\alpha\lor\beta)\equiv\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Expresión booleana: -\series default - -\begin_inset Formula $\alpha\lor(\neg\beta\land\beta)\equiv\alpha\land(\neg\beta\lor\beta)\equiv\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Reducción al absurdo: -\series default - -\begin_inset Formula $\neg\alpha\rightarrow(\beta\land\neg\beta)\equiv\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Propiedad de contraposición -\series default - o -\series bold -transposición: -\series default - -\begin_inset Formula $\alpha\rightarrow\beta\equiv\neg\beta\rightarrow\neg\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Exportación: -\series default - -\begin_inset Formula $(\alpha\land\beta)\rightarrow\gamma\equiv\alpha\rightarrow(\beta\rightarrow\gamma)$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Idempotencia: -\series default - -\begin_inset Formula $\alpha\equiv\neg(\neg\alpha)\equiv\alpha\lor\alpha\equiv\alpha\land\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Eliminación del condicional: -\series default - -\begin_inset Formula $\alpha\rightarrow\beta\equiv\neg\alpha\lor\beta\equiv\neg(\alpha\land\neg\beta)$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Eliminación del bicondicional: -\series default - -\begin_inset Formula $\alpha\leftrightarrow\beta\equiv(\alpha\rightarrow\beta)\land(\beta\rightarrow\alpha)\equiv(\alpha\land\beta)\lor(\neg\beta\land\neg\alpha)$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Propiedades sobre tautologías: -\series default - -\begin_inset Formula $\alpha\lor\neg\alpha\equiv V$ -\end_inset - -; -\begin_inset Formula $V\lor\beta\equiv V$ -\end_inset - -; -\begin_inset Formula $V\land\beta\equiv\beta$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Propiedades sobre insatisfacibilidad: -\series default - -\begin_inset Formula $\alpha\land\neg\alpha\equiv F$ -\end_inset - -; -\begin_inset Formula $F\lor\beta\equiv\beta$ -\end_inset - -; -\begin_inset Formula $F\land\beta\equiv F$ -\end_inset - -. -\end_layout - -\begin_layout Section -Razonamientos válidos -\end_layout - -\begin_layout Standard -Un razonamiento es válido si y sólo si en todas las interpretaciones en - las que -\begin_inset Formula $\alpha$ -\end_inset - - es verdad, -\begin_inset Formula $\beta$ -\end_inset - - también lo es. - Igualmente, -\begin_inset Formula $\beta$ -\end_inset - - es -\series bold -consecuencia lógica -\series default - de -\begin_inset Formula ${\cal F}=\{\alpha_{1},\dots,\alpha_{n}\}$ -\end_inset - - si -\begin_inset Formula $\beta$ -\end_inset - - es verdad siempre que -\begin_inset Formula ${\cal F}$ -\end_inset - - sea un modelo. - Escribimos -\begin_inset Formula $\alpha\vDash\beta$ -\end_inset - - o -\begin_inset Formula ${\cal F}\vDash\beta$ -\end_inset - -, y sabemos que -\begin_inset Formula $\alpha\vDash\beta\iff\vDash\alpha\rightarrow\beta$ -\end_inset - -. -\end_layout - -\begin_layout Standard - -\series bold -Teorema de la deducción semántica: -\series default - -\begin_inset Formula ${\cal F}\cup\{\alpha\}\vDash\beta\iff{\cal F}\vDash\alpha\rightarrow\beta$ -\end_inset - -. - Corolario: -\begin_inset Formula ${\cal F}\vDash\beta\iff\vDash\alpha_{1}\land\dots\land\alpha_{n}\rightarrow\beta\iff\vDash\neg(\alpha_{1}\land\dots\land\alpha_{n}\land\neg\beta)\iff\alpha_{1}\land\dots\land\alpha_{n}\land\neg\beta\text{ es insatisfacible}$ -\end_inset - -. - Propiedades generales de -\begin_inset Formula $\vDash$ -\end_inset - -: -\end_layout - -\begin_layout Itemize - -\series bold -Reflexividad: -\series default - -\begin_inset Formula $\alpha\vDash\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Transitividad: -\series default - Si -\begin_inset Formula ${\cal F}\vDash\alpha$ -\end_inset - - y -\begin_inset Formula $\alpha\vDash\beta$ -\end_inset - - entonces -\begin_inset Formula ${\cal F}\vDash\beta$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Monotonía: -\series default - Si -\begin_inset Formula ${\cal F}\vDash\alpha$ -\end_inset - - entonces -\begin_inset Formula ${\cal F}\cup\{\beta\}\vDash\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Itemize -Si -\begin_inset Formula ${\cal F}\vDash\alpha$ -\end_inset - - y -\begin_inset Formula $\vDash\beta$ -\end_inset - -, entonces -\begin_inset Formula ${\cal F}\backslash\{\beta\}\vDash\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Itemize -\begin_inset Formula $\alpha\equiv\beta\iff\alpha\vDash\beta\text{ y }\beta\vDash\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Standard -Algunas propiedades: -\end_layout - -\begin_layout Itemize - -\series bold -Simplificación -\series default - o -\series bold -eliminación de la conjunción: -\series default - -\begin_inset Formula $\alpha\land\beta\vDash\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Adición -\series default - o -\series bold -introducción de la disyunción: -\series default - -\begin_inset Formula $\alpha\vDash\alpha\lor\beta$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Silogismos: -\series default - Forma de razonamiento deductivo con dos premisas y una conclusión. -\end_layout - -\begin_deeper -\begin_layout Itemize - -\series bold -Categóricos -\end_layout - -\begin_deeper -\begin_layout Itemize - -\series bold -Combinación -\series default - o -\series bold -introducción de la conjunción: -\series default - -\begin_inset Formula $\{\alpha,\beta\}\vDash\alpha\land\beta$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Inconsistencia: -\series default - -\begin_inset Formula $\{\alpha,\neg\alpha\}\vDash\beta$ -\end_inset - -. -\end_layout - -\end_deeper -\begin_layout Itemize - -\series bold -Hipotéticos -\end_layout - -\begin_deeper -\begin_layout Itemize - -\series bold -Silogismo hipotético: -\series default - -\begin_inset Formula $\{\alpha\rightarrow\beta,\beta\rightarrow\gamma\}\vDash\alpha\rightarrow\gamma$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Demostración por casos: -\series default - -\begin_inset Formula $\{\alpha\rightarrow\gamma,\beta\rightarrow\gamma\}\vDash\alpha\lor\beta\rightarrow\gamma$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Prueba por casos: -\series default - -\begin_inset Formula $\{\alpha\rightarrow\beta,\neg\alpha\rightarrow\beta\}\vDash\beta$ -\end_inset - -. -\end_layout - -\end_deeper -\begin_layout Itemize - -\series bold -Hipotéticos mixtos -\end_layout - -\begin_deeper -\begin_layout Itemize - -\series bold -Modus Ponens: -\series default - -\begin_inset Formula $\{\alpha\rightarrow\beta,\alpha\}\vDash\beta$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Modus Tollens: -\series default - -\begin_inset Formula $\{\alpha\rightarrow\beta,\neg\beta\}\vDash\neg\alpha$ -\end_inset - -. -\end_layout - -\end_deeper -\begin_layout Itemize - -\series bold -Disyuntivo: -\series default - -\begin_inset Formula $\{\alpha\lor\beta,\neg\beta\}\vDash\alpha$ -\end_inset - -. -\end_layout - -\end_deeper -\begin_layout Itemize - -\series bold -Dilemas: -\series default - Forma de razonamiento con una premisa disyunción que representa las opciones, - normalmente contrarias. -\end_layout - -\begin_deeper -\begin_layout Itemize - -\series bold -Constructivo: -\series default - -\begin_inset Formula $\{\alpha\lor\beta,\alpha\rightarrow\gamma,\beta\rightarrow\delta\}\vDash\gamma\lor\delta$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Destructivo: -\series default - -\begin_inset Formula $\{\neg\gamma\lor\neg\delta,\alpha\rightarrow\gamma,\beta\rightarrow\delta\}\vDash\neg\alpha\lor\neg\beta$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Transposición: -\series default - -\begin_inset Formula $\alpha\rightarrow\beta\vDash\neg\beta\rightarrow\neg\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Eliminación de la equivalencia: -\series default - -\begin_inset Formula $\alpha\leftrightarrow\beta\vDash\{\alpha\rightarrow\beta,\beta\rightarrow\alpha\}$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Introducción de la equivalencia: -\series default - -\begin_inset Formula $\{\alpha\rightarrow\beta,\beta\rightarrow\alpha\}\vDash\alpha\leftrightarrow\beta$ -\end_inset - -. -\end_layout - -\end_deeper -\begin_layout Standard -El Corolario del Teorema de la Deducción Semántica y las propiedades básicas - de equivalencia y razonamientos nos permiten considerar al menos dos estrategia -s de razonamiento deductivo: la -\series bold -demostración directa -\series default -, comprobando que -\begin_inset Formula $\beta$ -\end_inset - - es consecuencia lógica de -\begin_inset Formula $\alpha$ -\end_inset - - mediante definiciones, tautologías, teoremas o propiedades, y -\series bold -refutación -\series default - o demostración por contradicción ( -\begin_inset Formula $\alpha\rightarrow\beta\equiv\alpha\land\neg\beta\implies\gamma\land\neg\gamma$ -\end_inset - -), buscando contraejemplos o encontrando un -\begin_inset Formula $a$ -\end_inset - - tal que -\begin_inset Formula $V(\alpha[a]\rightarrow\beta[a])=F$ -\end_inset - -. -\end_layout - -\end_body -\end_document diff --git a/logic/n3.lyx b/logic/n3.lyx deleted file mode 100644 index f720c27..0000000 --- a/logic/n3.lyx +++ /dev/null @@ -1,1512 +0,0 @@ -#LyX 2.3 created this file. For more info see http://www.lyx.org/ -\lyxformat 544 -\begin_document -\begin_header -\save_transient_properties true -\origin unavailable -\textclass book -\use_default_options true -\maintain_unincluded_children false -\language spanish -\language_package default -\inputencoding auto -\fontencoding global -\font_roman "default" "default" -\font_sans "default" "default" -\font_typewriter "default" "default" -\font_math "auto" "auto" -\font_default_family default -\use_non_tex_fonts false -\font_sc false -\font_osf false -\font_sf_scale 100 100 -\font_tt_scale 100 100 -\use_microtype false -\use_dash_ligatures true -\graphics default -\default_output_format default -\output_sync 0 -\bibtex_command default -\index_command default -\paperfontsize default -\spacing single -\use_hyperref false -\papersize default -\use_geometry false -\use_package amsmath 1 -\use_package amssymb 1 -\use_package cancel 1 -\use_package esint 1 -\use_package mathdots 1 -\use_package mathtools 1 -\use_package mhchem 1 -\use_package stackrel 1 -\use_package stmaryrd 1 -\use_package undertilde 1 -\cite_engine basic -\cite_engine_type default -\biblio_style plain -\use_bibtopic false -\use_indices false -\paperorientation portrait -\suppress_date false -\justification true -\use_refstyle 1 -\use_minted 0 -\index Index -\shortcut idx -\color #008000 -\end_index -\secnumdepth 3 -\tocdepth 3 -\paragraph_separation indent -\paragraph_indentation default -\is_math_indent 0 -\math_numbering_side default -\quotes_style swiss -\dynamic_quotes 0 -\papercolumns 1 -\papersides 1 -\paperpagestyle default -\tracking_changes false -\output_changes false -\html_math_output 0 -\html_css_as_file 0 -\html_be_strict false -\end_header - -\begin_body - -\begin_layout Section -Algoritmos que no requieren cláusulas -\end_layout - -\begin_layout Subsection -Tablas de verdad -\end_layout - -\begin_layout Standard -Construimos una tabla de verdad por filas, y si en una fila obtenemos que - la oración es cierta para dicha interpretación, la oración es satisfacible. - Si no es cierta en ninguna, la oración es insatisfacible. -\end_layout - -\begin_layout Subsection -Árboles semánticos -\end_layout - -\begin_layout Standard -Una hoja de un árbol semántico es un -\series bold -nodo fallo -\series default - si su etiqueta es -\begin_inset Formula $F$ -\end_inset - -, y -\series bold -nodo éxito -\series default - si es -\begin_inset Formula $V$ -\end_inset - -. - Representamos el árbol como -\begin_inset Formula $\vernal$ -\end_inset - -, y observamos que, para comprobar la satisfacibilidad, basta con encontrar - un nodo éxito, y entonces no es necesario seguir desarrollando. -\end_layout - -\begin_layout Subsection -Tableaux semánticos -\end_layout - -\begin_layout Standard -Un -\series bold -tableaux semántico -\series default - es un árbol en el cual cada nodo está formado por una lista de oraciones - (sin paréntesis de ningún tipo), y su raíz es la lista formada por la oración - -\begin_inset Formula $\phi$ -\end_inset - - a desarrollar. - Una oración puede tener -\series bold -comportamiento conjuntivo -\series default - (se le puede aplicar una -\begin_inset Formula $\alpha$ -\end_inset - --fórmula) o -\series bold -disyuntivo -\series default - (se le puede aplicar una -\begin_inset Formula $\beta$ -\end_inset - --fórmula), o ser un literal. - Para cada rama del árbol: -\end_layout - -\begin_layout Enumerate -Seleccionamos una oración que no sea un literal, preferiblemente con comportamie -nto conjuntivo. -\end_layout - -\begin_layout Enumerate -Si no encontramos ninguna, el nodo es un nodo hoja. - Lo marcamos como -\series bold -cerrado -\series default - si contiene un literal y su contrario, de lo contrario como -\series bold -abierto -\series default -. -\end_layout - -\begin_layout Enumerate -Si tiene comportamiento conjuntivo, aplicamos la -\begin_inset Formula $\alpha$ -\end_inset - --fórmula correspondiente y dibujamos una rama con la etiqueta -\begin_inset Formula $\alpha:\text{(nom. de fórmula)}$ -\end_inset - - y el nodo resultado de sustituir -\begin_inset Formula $\alpha,\phi_{1},\dots,\phi_{n}$ -\end_inset - - por -\begin_inset Formula $\alpha_{1},\alpha_{2},\phi_{1},\dots,\phi_{n}$ -\end_inset - -. -\end_layout - -\begin_layout Enumerate -Si tiene comportamiento disyuntivo, aplicamos la -\begin_inset Formula $\beta$ -\end_inset - --fórmula correspondiente y dibujamos dos ramas. - La división se marca con la etiqueta -\begin_inset Formula $\beta:\text{(nom. de fórmula)}$ -\end_inset - - y los nodos son los resultantes de sustituir -\begin_inset Formula $\beta,\phi_{1},\dots,\phi_{n}$ -\end_inset - - por -\begin_inset Formula $\beta_{1},\phi_{1},\dots,\phi_{n}$ -\end_inset - - y -\begin_inset Formula $\beta_{2},\phi_{1},\dots,\phi_{n}$ -\end_inset - -. -\end_layout - -\begin_layout Standard -\align center -\begin_inset Tabular - - - - - - - - - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\alpha$ -\end_inset - --fórmulas -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\beta$ -\end_inset - --fórmulas -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout - -\end_layout - -\end_inset - - - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\alpha$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\alpha_{1}$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\alpha_{2}$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\beta$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\beta_{1}$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\beta_{2}$ -\end_inset - - -\end_layout - -\end_inset - - - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\neg\neg\alpha$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\alpha$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout - -\end_layout - -\end_inset - - - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\alpha\land\beta$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\alpha$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\beta$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\neg(\alpha\land\beta)$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\neg\alpha$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\neg\beta$ -\end_inset - - -\end_layout - -\end_inset - - - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\neg(\alpha\lor\beta)$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\neg\alpha$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\neg\beta$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\alpha\lor\beta$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\alpha$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\beta$ -\end_inset - - -\end_layout - -\end_inset - - - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\neg(\alpha\rightarrow\beta)$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\alpha$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\neg\beta$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\alpha\rightarrow\beta$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\neg\alpha$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\beta$ -\end_inset - - -\end_layout - -\end_inset - - - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\alpha\leftrightarrow\beta$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\alpha\rightarrow\beta$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\beta\rightarrow\alpha$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\neg(\alpha\leftrightarrow\beta)$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\neg(\alpha\rightarrow\beta)$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\neg(\beta\rightarrow\alpha)$ -\end_inset - - -\end_layout - -\end_inset - - - - -\end_inset - - -\end_layout - -\begin_layout Standard -Un -\series bold -tableaux completado -\series default - o -\series bold -completo -\series default - es aquel cuya construcción ha terminado. - Decimos que es -\series bold -cerrado -\series default - cuando todas las hojas son cerradas, y -\series bold -abierto -\series default - cuando hay alguna abierta. - Así, -\begin_inset Formula $\phi$ -\end_inset - - es satisfacible si y sólo si su tableau completado es abierto. - Este método no detecta tautologías, pero podemos determinar que -\begin_inset Formula $\phi$ -\end_inset - - es tautológica cuando -\begin_inset Formula $\neg\phi$ -\end_inset - - es insatisfacible. -\end_layout - -\begin_layout Section -Algoritmos que requieren cláusulas -\end_layout - -\begin_layout Standard -Una fórmula -\begin_inset Formula $\xi$ -\end_inset - - está en -\series bold -forma normal conjuntiva -\series default - si es una cláusula o conjunción de cláusulas. - Una -\series bold -cláusula -\series default - es un literal o disyunción de dos o más literales (quitando todos los paréntesi -s). -\end_layout - -\begin_layout Itemize - -\series bold -Cláusula unitaria: -\series default - Con un solo literal. -\end_layout - -\begin_layout Itemize - -\series bold -Cláusula vacía: -\series default - Sin literales. - Se denota por -\begin_inset Formula $\square$ -\end_inset - - y es insatisfacible. -\end_layout - -\begin_layout Itemize - -\series bold -Cláusula de Horn: -\series default - Aquella que tiene como máximo un literal positivo. -\end_layout - -\begin_layout Standard -Llamamos -\series bold -conjunto clausal -\series default - o -\series bold -clausulado -\series default - al conjunto de dichas cláusulas, y decimos que está en -\series bold -forma clausal -\series default -. -\end_layout - -\begin_layout Subsection -Obtención de FNC -\end_layout - -\begin_layout Enumerate -Aplicar las reglas de eliminación de -\begin_inset Formula $\leftrightarrow$ -\end_inset - - y -\begin_inset Formula $\rightarrow$ -\end_inset - - hasta tener solo -\begin_inset Formula $\neg$ -\end_inset - -, -\begin_inset Formula $\land$ -\end_inset - - y -\begin_inset Formula $\lor$ -\end_inset - -. -\end_layout - -\begin_layout Enumerate -Aplicar De Morgan hasta que las negaciones solo afecten a átomos. -\end_layout - -\begin_layout Enumerate -Eliminar las negaciones múltiples ( -\begin_inset Formula $\neg\neg$ -\end_inset - -). -\end_layout - -\begin_layout Enumerate -Aplicar distributividad de -\begin_inset Formula $\lor$ -\end_inset - - sobre -\begin_inset Formula $\land$ -\end_inset - -. -\end_layout - -\begin_layout Enumerate -Reducir la cantidad de paréntesis. -\end_layout - -\begin_layout Standard -Si queremos simplificar: -\end_layout - -\begin_layout Enumerate -Eliminar literales opuestos: -\begin_inset Formula $\ell\lor\neg\ell\equiv V$ -\end_inset - -; -\begin_inset Formula $\ell\land\neg\ell\equiv F$ -\end_inset - -. -\end_layout - -\begin_layout Enumerate -Eliminar constantes y expresiones repetidas: -\begin_inset Formula $V\lor\alpha\equiv V$ -\end_inset - -; -\begin_inset Formula $F\lor\alpha\equiv V\land\alpha\equiv\alpha$ -\end_inset - -; -\begin_inset Formula $F\land\alpha\equiv F$ -\end_inset - -; -\begin_inset Formula $\alpha\lor\alpha\equiv\alpha\land\alpha\equiv\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Enumerate -Quedarnos con expresiones subsumidas: -\begin_inset Formula $(\alpha\lor\beta)\land\alpha\equiv\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Subsection -Algoritmo DPLL -\end_layout - -\begin_layout Standard -Al propagar un literal en una expresión en FNC, lo que hacemos es eliminar - las cláusulas en las que aparezca ( -\series bold -cláusula cancelada -\series default -) y las ocurrencias de literales complementarios ( -\series bold -ocurrencia eliminada -\series default -). - Al aplicar DPLL, representamos el conjunto clausulado como un conjunto - de conjuntos. - Por ejemplo, si -\begin_inset Formula $\phi\equiv p\land(q\lor\neg r)$ -\end_inset - -, entonces su conjunto clausal es -\begin_inset Formula $\Omega_{\phi}=\{p,q\lor\neg r\}$ -\end_inset - -, y lo representamos como -\begin_inset Formula $\Omega_{\phi FNC}=\{p,\{q,\neg r\}\}$ -\end_inset - -. - Entonces consideramos 5 reglas: -\end_layout - -\begin_layout Enumerate - -\series bold -Regla de la cláusula unitaria: -\series default - Si hay una cláusula unitaria, propagar su literal. -\end_layout - -\begin_layout Enumerate - -\series bold -Regla del literal puro: -\series default - Si hay un literal para el que no se da su complementario, propagarlo. -\end_layout - -\begin_layout Enumerate - -\series bold -Regla de la tautología: -\series default - Eliminar las cláusulas que contengan literales complementarios. -\end_layout - -\begin_layout Enumerate - -\series bold -Regla de la inclusión: -\series default - Si existen conjuntos clausales -\begin_inset Formula $C_{1},C_{2}\in\Omega_{\phi}$ -\end_inset - - tales que -\begin_inset Formula $C_{1}\subseteq C_{2}$ -\end_inset - -, eliminar -\begin_inset Formula $C_{2}$ -\end_inset - - de -\begin_inset Formula $\Omega_{\phi}$ -\end_inset - -. -\end_layout - -\begin_layout Enumerate - -\series bold -Regla de ramificación: -\series default - Considerar un literal -\begin_inset Formula $l$ -\end_inset - - (normalmente el que aparece más veces) y propagar -\begin_inset Formula $l$ -\end_inset - - por un lado y -\begin_inset Formula $\neg l$ -\end_inset - - por otro. -\end_layout - -\begin_layout Standard -El algoritmo consiste en: -\end_layout - -\begin_layout Enumerate -Si -\begin_inset Formula $\Omega_{\phi}=\{\}$ -\end_inset - -, devolver -\family typewriter -true -\family default - (se indica mediante una flecha de la expresión derivada a la original etiquetad -a -\begin_inset Quotes cld -\end_inset - -true -\begin_inset Quotes crd -\end_inset - -), indicando que es satisfacible. -\end_layout - -\begin_layout Enumerate -Si -\begin_inset Formula $\square\in\Omega_{\phi}$ -\end_inset - -, devolver -\family typewriter -false -\family default -. -\end_layout - -\begin_layout Enumerate -En caso contrario, aplicar la primera de las reglas que sea aplicable y - devolver su va -\begin_inset ERT -status open - -\begin_layout Plain Layout - - -\backslash -- -\end_layout - -\end_inset - -lor. - Para la regla de ramificación: Si la primera rama devuelve -\family typewriter -true -\family default -, devolverlo. - Si no, proceder con la segunda rama y devolver el valor devuelto. - Esto es lo que se denomina -\begin_inset Quotes cld -\end_inset - - -\lang american -backtracking -\lang spanish - -\begin_inset Quotes crd -\end_inset - - (a partir de un algoritmo recursivo). -\end_layout - -\begin_layout Standard -Lo representamos con un grafo, similar al del árbol semántico. -\end_layout - -\begin_layout Subsection -Método de resolución -\end_layout - -\begin_layout Standard -La -\series bold -resolvente -\series default - de dos cláusulas -\begin_inset Formula $\psi\equiv l_{1}\lor\dots\lor l_{n}\lor j$ -\end_inset - - y -\begin_inset Formula $\text{\phi}\equiv k_{1}\lor\dots\lor k_{m}\lor\neg j$ -\end_inset - - es la cláusula -\begin_inset Formula $R_{j}(\psi,\phi)\equiv l_{1}\lor\dots\lor l_{n}\lor k_{1}\lor\dots\lor k_{m}$ -\end_inset - -. - -\begin_inset Formula $\psi$ -\end_inset - - y -\begin_inset Formula $\phi$ -\end_inset - - son las -\series bold -cláusulas padres -\series default - de -\begin_inset Formula $R_{j}(\psi,\phi)$ -\end_inset - -, y -\begin_inset Formula $\{\psi,\phi\}$ -\end_inset - - es satisfacible si y sólo si -\begin_inset Formula $R_{j}(\psi,\phi)$ -\end_inset - - lo es. - Para resolver por resolución: -\end_layout - -\begin_layout Enumerate -Definimos el conjunto -\begin_inset Formula ${\cal C}=\Omega_{\phi}$ -\end_inset - - y -\begin_inset Formula ${\cal C}_{0}^{*}={\cal C}$ -\end_inset - -. -\end_layout - -\begin_layout Enumerate -Por cada par de cláusulas -\begin_inset Formula $C_{1}=l\lor\alpha$ -\end_inset - - y -\begin_inset Formula $C_{2}=\neg l\lor\beta$ -\end_inset - - en -\begin_inset Formula ${\cal C}^{*}$ -\end_inset - -, obtenemos su resolvente y la añadimos a -\begin_inset Formula ${\cal C}^{*}$ -\end_inset - -. - Si obtenemos la resolvente -\begin_inset Formula $\square$ -\end_inset - -, el conjunto -\begin_inset Formula ${\cal C}^{*}$ -\end_inset - - es insatisfacible y por tanto -\begin_inset Formula ${\cal C}$ -\end_inset - - también. -\end_layout - -\begin_layout Enumerate -Una vez obtenidas todas las resolventes, si -\begin_inset Formula $\square\notin{\cal C}^{*}$ -\end_inset - -, entonces -\begin_inset Formula ${\cal C}^{*}$ -\end_inset - - es satisfacible y por tanto -\begin_inset Formula ${\cal C}$ -\end_inset - - también (solo en L0). -\end_layout - -\begin_layout Standard -Podemos expresar este algoritmo mediante un -\series bold -grafo de resolución -\series default -, en el que de cada par de cláusulas posible parte una línea hacia abajo - hacia su resolvente y tenemos cuidado de no incluir un resolvente igual - a una cláusula ya existente. -\end_layout - -\begin_layout Standard -En dicho grafo, las premisas se dice que están en el nivel 0 ( -\begin_inset Formula ${\cal C}$ -\end_inset - -), y si -\begin_inset Formula $C_{1}$ -\end_inset - - y -\begin_inset Formula $C_{2}$ -\end_inset - - están en los niveles -\begin_inset Formula $x_{1}$ -\end_inset - - y -\begin_inset Formula $x_{2}$ -\end_inset - -, su resolvente está en el nivel -\begin_inset Formula $\max\{x_{1},x_{2}\}+1$ -\end_inset - -, de forma que cada nivel se representa en una misma línea horizontal, y - los resolventes se numeran empezando por el nivel más alto (el nivel 0). -\end_layout - -\begin_layout Standard -Un grafo de resolución es -\series bold -básico -\series default - si solo muestra dos cláusulas y su resolvente; -\series bold -completo -\series default - si contiene la unión de todos los grafos de resolución básicos, y es un - -\series bold -grafo de refutación -\series default - si aparece -\begin_inset Formula $\square$ -\end_inset - -. -\end_layout - -\begin_layout Standard -Para la elección de los pares de cláusulas padres, existen principalmente - dos -\series bold -estrategias de resolución: -\end_layout - -\begin_layout Itemize - -\series bold -Búsqueda en anchura: -\series default - Se obtienen todas las resolventes de un nivel antes de pasar al siguiente. - Orden -\begin_inset Formula $(2,1)$ -\end_inset - -, -\begin_inset Formula $(3,1)$ -\end_inset - -, -\begin_inset Formula $(3,2)$ -\end_inset - -, -\begin_inset Formula $(4,1)$ -\end_inset - -, etc. -\end_layout - -\begin_layout Itemize - -\series bold -Búsqueda en profundidad: -\series default - Una vez obtenida una resolvente de nivel -\begin_inset Formula $i$ -\end_inset - -, intenta obtener una de nivel -\begin_inset Formula $i+1$ -\end_inset - - a partir de ella. - Orden -\begin_inset Formula $(2,1)\rightarrow i$ -\end_inset - -, -\begin_inset Formula $(i,1)$ -\end_inset - -, -\begin_inset Formula $(i,2)$ -\end_inset - -, -\begin_inset Formula $(i,3)\rightarrow j$ -\end_inset - -, -\begin_inset Formula $(j,1)$ -\end_inset - -, etc. - No es completa. -\end_layout - -\begin_layout Standard -En la práctica se utiliza la -\series bold -notación -\series default - o -\series bold -representación Fitting -\series default -: Se crea una lista numerada de las cláusulas de -\begin_inset Formula ${\cal C}$ -\end_inset - -, con la indicación -\begin_inset Quotes cld -\end_inset - -Premisa -\begin_inset Quotes crd -\end_inset - - o -\begin_inset Quotes cld -\end_inset - -C.E. -\begin_inset Quotes crd -\end_inset - - (conjunto de entrada) a la derecha de cada una. - Después, se van comprobando los pares de cláusulas en la lista, empezando - por -\begin_inset Formula $(2,1)$ -\end_inset - -, -\begin_inset Formula $(3,1)$ -\end_inset - -, -\begin_inset Formula $(3,2)$ -\end_inset - -, etc., y se va ampliando con los resolventes, que tendrán la indicación - -\begin_inset Formula $R_{l}(i,j)$ -\end_inset - -, siendo -\begin_inset Formula $i$ -\end_inset - - y -\begin_inset Formula $j$ -\end_inset - - los ordinales de las cláusulas padres. - Para optimizar, se pueden tachar cláusulas por los siguientes motivos: -\end_layout - -\begin_layout Itemize -Literal puro ( -\begin_inset Formula $l$ -\end_inset - -) [después de tachar ( -\begin_inset Formula $n$ -\end_inset - -)]. -\end_layout - -\begin_layout Itemize -Subsumida en ( -\begin_inset Formula $n$ -\end_inset - -). -\end_layout - -\begin_layout Itemize -Tautología ( -\begin_inset Formula $l\lor\neg l$ -\end_inset - -). -\end_layout - -\begin_layout Standard -El motivo debe indicarse a la derecha. - Si al final queda -\begin_inset Formula ${\cal C}^{*}=\{\}$ -\end_inset - -, la oración es satisfacible. -\end_layout - -\begin_layout Section -Razonamiento automático -\end_layout - -\begin_layout Standard -Un razonamiento es válido ( -\begin_inset Formula $\{\alpha_{1},\dots,\alpha_{n}\}\vDash\beta$ -\end_inset - -) cuando -\begin_inset Formula $\vDash\alpha_{1}\land\dots\land\alpha_{n}\rightarrow\beta$ -\end_inset - -, es decir, cuando -\begin_inset Formula $\alpha_{1}\land\dots\land\alpha_{n}\land\neg\beta$ -\end_inset - - es insatisfacible. - Así, mediante tablas de verdad o árboles semánticos, podemos determinar - la validez de un razonamiento demostrando que -\begin_inset Formula $\alpha_{1}\land\dots\land\alpha_{n}\rightarrow\beta$ -\end_inset - - es una tautología. - Para el resto de los métodos, comprobamos que -\begin_inset Formula $\alpha_{1}\land\dots\land\alpha_{n}\land\neg\beta$ -\end_inset - - es una contradicción. -\end_layout - -\begin_layout Standard -En el caso de demostración por resolución, las cláusulas de -\begin_inset Formula $\neg\beta$ -\end_inset - - se denominan -\begin_inset Quotes cld -\end_inset - -conjunto soporte de entrada -\begin_inset Quotes crd -\end_inset - -. - Se marcan con un -\begin_inset Formula $*$ -\end_inset - - a la izquierda del ordinal tanto estas como las resolventes de alguna cláusula - marcada con -\begin_inset Formula $*$ -\end_inset - -, de forma recursiva. -\end_layout - -\end_body -\end_document diff --git a/logic/n4.lyx b/logic/n4.lyx deleted file mode 100644 index 3796419..0000000 --- a/logic/n4.lyx +++ /dev/null @@ -1,402 +0,0 @@ -#LyX 2.3 created this file. For more info see http://www.lyx.org/ -\lyxformat 544 -\begin_document -\begin_header -\save_transient_properties true -\origin unavailable -\textclass book -\use_default_options true -\maintain_unincluded_children false -\language spanish -\language_package default -\inputencoding auto -\fontencoding global -\font_roman "default" "default" -\font_sans "default" "default" -\font_typewriter "default" "default" -\font_math "auto" "auto" -\font_default_family default -\use_non_tex_fonts false -\font_sc false -\font_osf false -\font_sf_scale 100 100 -\font_tt_scale 100 100 -\use_microtype false -\use_dash_ligatures true -\graphics default -\default_output_format default -\output_sync 0 -\bibtex_command default -\index_command default -\paperfontsize default -\spacing single -\use_hyperref false -\papersize default -\use_geometry false -\use_package amsmath 1 -\use_package amssymb 1 -\use_package cancel 1 -\use_package esint 1 -\use_package mathdots 1 -\use_package mathtools 1 -\use_package mhchem 1 -\use_package stackrel 1 -\use_package stmaryrd 1 -\use_package undertilde 1 -\cite_engine basic -\cite_engine_type default -\biblio_style plain -\use_bibtopic false -\use_indices false -\paperorientation portrait -\suppress_date false -\justification true -\use_refstyle 1 -\use_minted 0 -\index Index -\shortcut idx -\color #008000 -\end_index -\secnumdepth 3 -\tocdepth 3 -\paragraph_separation indent -\paragraph_indentation default -\is_math_indent 0 -\math_numbering_side default -\quotes_style swiss -\dynamic_quotes 0 -\papercolumns 1 -\papersides 1 -\paperpagestyle default -\tracking_changes false -\output_changes false -\html_math_output 0 -\html_css_as_file 0 -\html_be_strict false -\end_header - -\begin_body - -\begin_layout Standard -Las expresiones, numeradas, están dentro de una caja, que se representa - con los tres bordes de arriba, abajo y a la izquierda (a la derecha del - número de línea). - La caja principal no se suele representar. - Si se usa una -\emph on -Hipótesis -\emph default -, se crea una nueva caja (dentro de otra), y en cada caja las -\emph on -Premisas -\emph default - o -\emph on -Hipótesis -\emph default - van al principio y la última línea es la conclusión. - Cada caja representa una deducción ( -\begin_inset Formula $\vdash$ -\end_inset - -). -\end_layout - -\begin_layout Section -Reglas -\end_layout - -\begin_layout Standard -\align center -\begin_inset Tabular - - - - - - - -\begin_inset Text - -\begin_layout Plain Layout - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -Eliminación de -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -Introducción de -\end_layout - -\end_inset - - - - -\begin_inset Text - -\begin_layout Plain Layout -la conjunción -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $E_{\land}:\frac{\vdash\alpha\land\beta}{\vdash\alpha},\frac{\vdash\alpha\land\beta}{\vdash\beta}$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $I_{\land}:\frac{\vdash\alpha\,\vdash\beta}{\vdash\alpha\land\beta}$ -\end_inset - - -\end_layout - -\end_inset - - - - -\begin_inset Text - -\begin_layout Plain Layout -la disyunción -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\underset{\text{Prueba por casos}}{E_{\lor}:\frac{\vdash\alpha\lor\beta\,\vdash(\alpha\vdash\gamma)\,\vdash(\beta\vdash\gamma)}{\vdash\gamma}}$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $I_{\lor}:\frac{\vdash\alpha}{\vdash\alpha\lor\beta},\frac{\vdash\alpha}{\vdash\beta\lor\alpha}$ -\end_inset - - -\end_layout - -\end_inset - - - - -\begin_inset Text - -\begin_layout Plain Layout -la implicación -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\underset{\text{Modus Ponens}}{E_{\rightarrow}:\frac{\vdash\alpha\rightarrow\beta\,\vdash\alpha}{\vdash\beta}}$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\underset{\text{Teorema de la Deducción}}{I_{\rightarrow}:\frac{\vdash(\alpha\vdash\beta)}{\vdash\alpha\rightarrow\beta}}$ -\end_inset - - -\end_layout - -\end_inset - - - - -\begin_inset Text - -\begin_layout Plain Layout -la doble implicación -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $E_{\leftrightarrow}:\frac{\vdash(\alpha\leftrightarrow\beta)}{\vdash(\alpha\rightarrow\beta)},\frac{\vdash(\alpha\leftrightarrow\beta)}{\vdash(\beta\rightarrow\alpha)}$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $I_{\leftrightarrow}:\frac{\vdash(\alpha\rightarrow\beta)\,\vdash(\beta\rightarrow\alpha)}{\vdash(\alpha\leftrightarrow\beta)}$ -\end_inset - - -\end_layout - -\end_inset - - - - -\begin_inset Text - -\begin_layout Plain Layout -la negación -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\underset{\text{Reducción al absurdo}}{E_{\neg}:\frac{\vdash(\neg\alpha\vdash\beta\land\neg\beta)}{\vdash\alpha}}$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\underset{\text{Reducción al absurdo}}{I_{\neg}:\frac{\vdash(\alpha\vdash\beta\land\neg\beta)}{\vdash\neg\alpha}}$ -\end_inset - - -\end_layout - -\end_inset - - - - -\begin_inset Text - -\begin_layout Plain Layout -la doble negación -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $E_{\neg\neg}:\frac{\vdash\neg\neg\alpha}{\vdash\alpha}$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout - -\end_layout - -\end_inset - - - - -\begin_inset Text - -\begin_layout Plain Layout -la contradicción -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $CONTRA:\frac{\vdash\alpha\,\vdash\neg\alpha}{\vdash\beta}$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout - -\end_layout - -\end_inset - - - - -\end_inset - - -\end_layout - -\begin_layout Standard -También la iteración: -\begin_inset Formula $IT:\frac{\vdash\alpha}{\vdash\alpha}$ -\end_inset - -, que se usa cuando la hipótesis de una caja es la conclusión, dado que - deben estar en líneas distintas. -\end_layout - -\end_body -\end_document diff --git a/logic/n5.lyx b/logic/n5.lyx deleted file mode 100644 index e887da2..0000000 --- a/logic/n5.lyx +++ /dev/null @@ -1,660 +0,0 @@ -#LyX 2.3 created this file. For more info see http://www.lyx.org/ -\lyxformat 544 -\begin_document -\begin_header -\save_transient_properties true -\origin unavailable -\textclass book -\use_default_options true -\maintain_unincluded_children false -\language spanish -\language_package default -\inputencoding auto -\fontencoding global -\font_roman "default" "default" -\font_sans "default" "default" -\font_typewriter "default" "default" -\font_math "auto" "auto" -\font_default_family default -\use_non_tex_fonts false -\font_sc false -\font_osf false -\font_sf_scale 100 100 -\font_tt_scale 100 100 -\use_microtype false -\use_dash_ligatures true -\graphics default -\default_output_format default -\output_sync 0 -\bibtex_command default -\index_command default -\paperfontsize default -\spacing single -\use_hyperref false -\papersize default -\use_geometry false -\use_package amsmath 1 -\use_package amssymb 1 -\use_package cancel 1 -\use_package esint 1 -\use_package mathdots 1 -\use_package mathtools 1 -\use_package mhchem 1 -\use_package stackrel 1 -\use_package stmaryrd 1 -\use_package undertilde 1 -\cite_engine basic -\cite_engine_type default -\biblio_style plain -\use_bibtopic false -\use_indices false -\paperorientation portrait -\suppress_date false -\justification true -\use_refstyle 1 -\use_minted 0 -\index Index -\shortcut idx -\color #008000 -\end_index -\secnumdepth 3 -\tocdepth 3 -\paragraph_separation indent -\paragraph_indentation default -\is_math_indent 0 -\math_numbering_side default -\quotes_style swiss -\dynamic_quotes 0 -\papercolumns 1 -\papersides 1 -\paperpagestyle default -\tracking_changes false -\output_changes false -\html_math_output 0 -\html_css_as_file 0 -\html_be_strict false -\end_header - -\begin_body - -\begin_layout Section -Conjuntos -\end_layout - -\begin_layout Standard -Una -\series bold -categoría -\series default - o -\series bold -conjunto -\series default - es una colección no ordenada de -\series bold -elementos -\series default -. - Se dice que un elemento -\begin_inset Formula $x$ -\end_inset - - pertenece al conjunto -\begin_inset Formula $C$ -\end_inset - -, y se representa como -\begin_inset Formula $x\in C$ -\end_inset - - (negación: -\begin_inset Formula $x\notin C$ -\end_inset - -) o -\begin_inset Formula $C(x)$ -\end_inset - -. - Podemos definir un conjunto por extensión ( -\begin_inset Formula $C=\{x_{1},x_{2},\dots\}$ -\end_inset - -), intensión ( -\begin_inset Formula $C=\{x|P(x)\}$ -\end_inset - -) o recursión ( -\begin_inset Formula $C=\{x|R(x)\}$ -\end_inset - -). -\end_layout - -\begin_layout Itemize - -\series bold -Igualdad: -\series default - -\begin_inset Formula $A=B:\iff(x\in A\iff x\in B)$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Inclusión: -\series default - -\begin_inset Formula $A\subseteq B:\iff(x\in A\implies x\in B)$ -\end_inset - - (negación: -\begin_inset Formula $A\nsubseteq B$ -\end_inset - -). -\end_layout - -\begin_layout Itemize - -\series bold -Inclusión estricta: -\series default - -\begin_inset Formula $A\subsetneq B:\iff(A\subseteq B\text{ y }A\neq B$ -\end_inset - -). -\end_layout - -\begin_layout Itemize - -\series bold -Conjunto total -\series default - o -\series bold -universo: -\series default - -\begin_inset Formula ${\cal U}$ -\end_inset - -, el mayor conjunto que podemos considerar para un estudio. -\end_layout - -\begin_layout Itemize - -\series bold -Conjunto vacío: -\series default - -\begin_inset Formula $\emptyset=\{\}$ -\end_inset - -, sin elementos. -\end_layout - -\begin_layout Itemize - -\series bold -Partes: -\series default - -\begin_inset Formula ${\cal P}(X)=\{A|A\subseteq X\}$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Unión: -\series default - -\begin_inset Formula $A\cup B:=\{x|x\in A\text{ ó }x\in B\}$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Intersección: -\series default - -\begin_inset Formula $A\cap B:=\{x|x\in A\text{ y }x\in B\}$ -\end_inset - -. - Si -\begin_inset Formula $A\cap B=\emptyset$ -\end_inset - -, -\begin_inset Formula $A$ -\end_inset - - y -\begin_inset Formula $B$ -\end_inset - - son -\series bold -disjuntos -\series default -. -\end_layout - -\begin_layout Itemize - -\series bold -Diferencia: -\series default - -\begin_inset Formula $A-B:=A\backslash B:=\{x|x\in A\text{ y }x\notin B\}$ -\end_inset - - -\end_layout - -\begin_layout Itemize - -\series bold -Complemento: -\series default - -\begin_inset Formula $\overline{A}:=A^{\complement}:={\cal U}\backslash A$ -\end_inset - -. -\end_layout - -\begin_layout Standard -Un -\series bold -diagrama de Euler -\series default - representa los conjuntos como círculos bien unos dentro de otros, separados - o intersecados, indicando de esta forma sus relaciones. - Un -\series bold -diagrama de Venn -\series default - representa los conjuntos como círculos todos intersecados entre sí, con - las partes no vacías sombreadas. -\end_layout - -\begin_layout Standard -Una -\series bold -familia de conjuntos -\series default - -\begin_inset Formula ${\cal A}$ -\end_inset - - es un conjunto formado solo por conjuntos, y es una -\series bold -partición -\series default - de -\begin_inset Formula $A$ -\end_inset - - si y sólo si -\begin_inset Formula $\bigcup{\cal A}=A$ -\end_inset - - y si para todo -\begin_inset Formula $B,C\in{\cal A}$ -\end_inset - - con -\begin_inset Formula $B\neq C$ -\end_inset - - se tiene que -\begin_inset Formula $B\cap C=\emptyset$ -\end_inset - -. -\end_layout - -\begin_layout Section -Sintaxis -\end_layout - -\begin_layout Standard -Extensión de la lógica proposicional. - Las proposiciones atómicas tienen la forma -\begin_inset Formula $P(x)$ -\end_inset - -, donde -\begin_inset Formula $P$ -\end_inset - - es una categoría y -\begin_inset Formula $x$ -\end_inset - - una variable (ambas conjuntos de letras latinas), y se leen -\begin_inset Quotes cld -\end_inset - - -\begin_inset Formula $x$ -\end_inset - - es -\begin_inset Formula $P$ -\end_inset - - -\begin_inset Quotes crd -\end_inset - -. - Además, se añaden los cuantificadores -\begin_inset Formula $\forall x$ -\end_inset - - (para todo -\begin_inset Formula $x$ -\end_inset - -) y -\begin_inset Formula $\exists x$ -\end_inset - - (existe -\begin_inset Formula $x$ -\end_inset - -), donde -\begin_inset Formula $x$ -\end_inset - - puede ser cualquier variable. - Estos tienen la misma prioridad que la negación. - Las proposiciones compuestas se forman mediante cuatro -\series bold -formas normales: -\end_layout - -\begin_layout Itemize - -\series bold -Universal afirmativa: -\series default - -\begin_inset Formula $\forall x(P(x)\rightarrow Q(x))$ -\end_inset - -; -\begin_inset Quotes cld -\end_inset - -todo -\begin_inset Formula $P$ -\end_inset - - es -\begin_inset Formula $Q$ -\end_inset - - -\begin_inset Quotes crd -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Universal negativa: -\series default - -\begin_inset Formula $\forall x(P(x)\rightarrow\neg Q(x))$ -\end_inset - -; -\begin_inset Quotes cld -\end_inset - -ningún -\begin_inset Formula $P$ -\end_inset - - es -\begin_inset Formula $Q$ -\end_inset - - -\begin_inset Quotes crd -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Existencial afirmativa: -\series default - -\begin_inset Formula $\exists x(P(x)\land Q(x))$ -\end_inset - -; -\begin_inset Quotes cld -\end_inset - -algún -\begin_inset Formula $P$ -\end_inset - - es -\begin_inset Formula $Q$ -\end_inset - - -\begin_inset Quotes crd -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Existencial negativa: -\series default - -\begin_inset Formula $\exists x(P(x)\land\neg Q(x))$ -\end_inset - -; -\begin_inset Quotes cld -\end_inset - -algún -\begin_inset Formula $P$ -\end_inset - - no es -\begin_inset Formula $Q$ -\end_inset - - -\begin_inset Quotes crd -\end_inset - -. -\end_layout - -\begin_layout Section -Evaluación -\end_layout - -\begin_layout Standard -Para evaluar una proposición en LC interpretada en un mundo -\begin_inset Formula ${\cal M}$ -\end_inset - -: -\end_layout - -\begin_layout Enumerate -Definimos -\begin_inset Formula ${\cal U}$ -\end_inset - - como el conjunto de todos los elementos que aparecen en -\begin_inset Formula ${\cal M}$ -\end_inset - -. -\end_layout - -\begin_layout Enumerate -Identificamos cada categoría -\begin_inset Formula $P$ -\end_inset - - con un conjunto -\begin_inset Formula $P_{{\cal M}}$ -\end_inset - - del mundo. - El resultado es la -\series bold -interpretación -\series default - -\begin_inset Formula $I=\{P\mapsto P_{{\cal M}},\dots\}$ -\end_inset - -. -\end_layout - -\begin_layout Enumerate -Evaluamos el valor de verdad de la proposición a partir de la interpretación. - Para ello: -\end_layout - -\begin_deeper -\begin_layout Enumerate -Si encontramos un -\begin_inset Formula $\forall x\alpha[x]$ -\end_inset - -, decimos que esto es verdad si para cualquier -\begin_inset Formula $x\looparrowright d$ -\end_inset - - se cumple -\begin_inset Formula $V(\alpha[d])=V$ -\end_inset - -. - Aquí, -\begin_inset Formula $\alpha[d]\equiv\{\alpha[x]\}_{d/x}$ -\end_inset - - el resultado de aplicar la -\series bold -sustitución -\series default - -\begin_inset Formula $\{d/x\}$ -\end_inset - -. - Entonces comprobamos -\begin_inset Formula $V(\alpha[d])$ -\end_inset - - para todo -\begin_inset Formula $x\looparrowright d$ -\end_inset - - ( -\series bold -asignación -\series default -) con -\begin_inset Formula $d\in{\cal U}$ -\end_inset - - hasta encontrar un caso donde -\begin_inset Formula $V(\alpha[d])=F$ -\end_inset - - (con lo que -\begin_inset Formula $V(\forall x\alpha[x])=F$ -\end_inset - -) o llegar a que en todos -\begin_inset Formula $V(\alpha[d])=V$ -\end_inset - - (con lo que -\begin_inset Formula $V(\forall x\alpha[x])=V$ -\end_inset - -). -\end_layout - -\begin_layout Enumerate -Si encontramos un -\begin_inset Formula $\exists x\alpha[x]$ -\end_inset - - decimos que esto es verdad si encontramos un -\begin_inset Formula $x\looparrowright d$ -\end_inset - - para el que -\begin_inset Formula $V(\alpha[d])=V$ -\end_inset - -. - Entonces comprobamos -\begin_inset Formula $V(\alpha[d])$ -\end_inset - - para todo -\begin_inset Formula $x\looparrowright d$ -\end_inset - - con -\begin_inset Formula $d\in{\cal U}$ -\end_inset - - hasta encontrar un caso donde -\begin_inset Formula $V(\alpha[d])=V$ -\end_inset - - (con lo que -\begin_inset Formula $V(\exists x\alpha[x])=V$ -\end_inset - -) o llegar a que todos son falsos (con lo que -\begin_inset Formula $V(\exists x\alpha[x])=F$ -\end_inset - -). -\end_layout - -\end_deeper -\end_body -\end_document diff --git a/logic/n6.lyx b/logic/n6.lyx deleted file mode 100644 index f89c446..0000000 --- a/logic/n6.lyx +++ /dev/null @@ -1,1406 +0,0 @@ -#LyX 2.3 created this file. For more info see http://www.lyx.org/ -\lyxformat 544 -\begin_document -\begin_header -\save_transient_properties true -\origin unavailable -\textclass book -\use_default_options true -\maintain_unincluded_children false -\language spanish -\language_package default -\inputencoding auto -\fontencoding global -\font_roman "default" "default" -\font_sans "default" "default" -\font_typewriter "default" "default" -\font_math "auto" "auto" -\font_default_family default -\use_non_tex_fonts false -\font_sc false -\font_osf false -\font_sf_scale 100 100 -\font_tt_scale 100 100 -\use_microtype false -\use_dash_ligatures true -\graphics default -\default_output_format default -\output_sync 0 -\bibtex_command default -\index_command default -\paperfontsize default -\spacing single -\use_hyperref false -\papersize default -\use_geometry false -\use_package amsmath 1 -\use_package amssymb 1 -\use_package cancel 1 -\use_package esint 1 -\use_package mathdots 1 -\use_package mathtools 1 -\use_package mhchem 1 -\use_package stackrel 1 -\use_package stmaryrd 1 -\use_package undertilde 1 -\cite_engine basic -\cite_engine_type default -\biblio_style plain -\use_bibtopic false -\use_indices false -\paperorientation portrait -\suppress_date false -\justification true -\use_refstyle 1 -\use_minted 0 -\index Index -\shortcut idx -\color #008000 -\end_index -\secnumdepth 3 -\tocdepth 3 -\paragraph_separation indent -\paragraph_indentation default -\is_math_indent 0 -\math_numbering_side default -\quotes_style swiss -\dynamic_quotes 0 -\papercolumns 1 -\papersides 1 -\paperpagestyle default -\tracking_changes false -\output_changes false -\html_math_output 0 -\html_css_as_file 0 -\html_be_strict false -\end_header - -\begin_body - -\begin_layout Section -Relaciones -\end_layout - -\begin_layout Standard -La lógica de primer orden (L1) extiende la lógica categórica permitiendo - expresar relaciones fuera de las formas normales y relaciones de varios - objetos. - Podemos distinguir: -\end_layout - -\begin_layout Itemize - -\series bold -Categorías: -\series default - -\begin_inset Quotes cld -\end_inset - - -\begin_inset Formula $x$ -\end_inset - - es -\begin_inset Formula $P$ -\end_inset - - -\begin_inset Quotes crd -\end_inset - -, -\begin_inset Formula $x\in P$ -\end_inset - -, -\begin_inset Formula $P(r)$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Relaciones binarias: -\series default - -\begin_inset Quotes cld -\end_inset - - -\begin_inset Formula $x$ -\end_inset - - e -\begin_inset Formula $y$ -\end_inset - - son -\begin_inset Formula $R$ -\end_inset - - -\begin_inset Quotes crd -\end_inset - -, -\begin_inset Quotes cld -\end_inset - - -\begin_inset Formula $x$ -\end_inset - - se relaciona con -\begin_inset Formula $y$ -\end_inset - - -\begin_inset Quotes crd -\end_inset - -, -\begin_inset Formula $(x,y)\in R$ -\end_inset - -, -\begin_inset Formula $R(x,y)$ -\end_inset - -, -\begin_inset Formula $xRy$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Relaciones -\series default - de cualquier orden: -\begin_inset Formula $(x_{1},\dots,x_{n})\in S$ -\end_inset - -, -\begin_inset Formula $S(x_{1},\dots,x_{n})$ -\end_inset - -. - Se dice que -\begin_inset Formula $S$ -\end_inset - - tiene -\series bold -aridad -\series default - -\begin_inset Formula $n$ -\end_inset - -, o que es una relación -\series bold - -\begin_inset Formula $n$ -\end_inset - --aria -\series default -, lo que se representa por -\begin_inset Formula $S/n$ -\end_inset - -. - En general, -\begin_inset Formula $Q$ -\end_inset - - es una relación -\begin_inset Formula $n$ -\end_inset - --aria entre -\begin_inset Formula $A_{1},\dots,A_{n}$ -\end_inset - - si -\begin_inset Formula $Q\subseteq\prod_{i=1}^{n}A_{i}$ -\end_inset - -. - Si -\begin_inset Formula $\forall i,A_{i}=A$ -\end_inset - -, entonces -\begin_inset Formula $\prod_{i=1}^{n}A_{i}=A^{n}$ -\end_inset - -. -\end_layout - -\begin_layout Standard -En relaciones con aridad -\begin_inset Formula $n\geq2$ -\end_inset - -, se define el -\series bold -dominio -\series default - como -\begin_inset Formula $\text{Dom}(R)=\{(x_{1},\dots,x_{n-1})|\exists x_{n}:(x_{1},\dots,x_{n})\in R\}$ -\end_inset - - (si la aridad es -\begin_inset Formula $2$ -\end_inset - -, entonces -\begin_inset Formula $\text{Dom}(R)=\{x|\exists y:xRy\}$ -\end_inset - -), y el -\series bold -rango -\series default - como -\begin_inset Formula $\text{Ran}(R)=\{x_{n}|\exists(x_{1},\dots,x_{n-1}):(x_{1},\dots,x_{n})\in R\}$ -\end_inset - - (si la aridad es -\begin_inset Formula $2$ -\end_inset - -, entonces -\begin_inset Formula $\text{Ran}(R)=\{y|\exists x:xRy\}$ -\end_inset - -. - El -\series bold -campo -\series default - de -\begin_inset Formula $R$ -\end_inset - - se define como -\begin_inset Formula $\text{Campo}(R)=\text{Dom}(R)\cup\text{Ran}(R)$ -\end_inset - -. - Representaciones: -\end_layout - -\begin_layout Itemize - -\series bold -Cartesiana: -\series default - Similar a una función, con el conjunto inicial en el eje horizontal. - Se marcan los puntos que están en -\begin_inset Formula $R$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Tabular: -\series default - Como la cartesiana pero en una tabla. - En cada celda se pone un -\begin_inset Formula $1$ -\end_inset - - si el producto de tipos está en -\begin_inset Formula $R$ -\end_inset - -, un -\begin_inset Formula $0$ -\end_inset - - si no está y se deja en blanco si no lo sabemos. -\end_layout - -\begin_layout Itemize - -\series bold -Mediante digrafo: -\series default - Se representa a la izquierda el conjunto inicial y a la derecha el final, - y las relaciones se representan con flechas entre elementos de cada. -\end_layout - -\begin_layout Itemize - -\series bold -Grafo dirigido: -\series default - Se representa -\begin_inset Formula ${\cal U}$ -\end_inset - - y se indican las relaciones binarias con flechas. -\end_layout - -\begin_layout Standard -Una relación -\begin_inset Formula $n$ -\end_inset - --aria -\begin_inset Formula $f$ -\end_inset - - es una -\series bold -función -\series default - si y sólo si para cada elemento -\begin_inset Formula $x\in\text{Dom}(f)$ -\end_inset - - existe un único -\begin_inset Formula $y\in\text{Ran}(f)$ -\end_inset - - que se relacione con él. - Se escribe -\begin_inset Formula $f(x)=y$ -\end_inset - -, y la función se representa como -\begin_inset Formula $f:\prod_{i=1}^{n-1}A_{i}\rightarrow A_{n}$ -\end_inset - -. - Es -\series bold -inyectiva -\series default - si -\begin_inset Formula $f(x)=f(x')\implies x=x'$ -\end_inset - -, -\series bold -suprayectiva -\series default - si -\begin_inset Formula $\text{Ran}(f)=A_{n}$ -\end_inset - - y -\series bold -biyectiva -\series default - si es inyectiva y suprayectiva. - Definimos la aridad de -\begin_inset Formula $f$ -\end_inset - - como función como -\begin_inset Formula $n-1$ -\end_inset - -. -\end_layout - -\begin_layout Standard -\begin_inset Note Comment -status open - -\begin_layout Plain Layout -Tipos de relaciones: -\end_layout - -\begin_layout Itemize - -\series bold -Reflexiva: -\series default - -\begin_inset Formula $\forall a\in A,aRa$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Irreflexiva: -\series default - -\begin_inset Formula $\forall a\in A,a\not Ra$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Serial: -\series default - -\begin_inset Formula $\forall a\in A,\exists b\in A:aRb$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Simétrica: -\series default - -\begin_inset Formula $\forall a,b\in A,(aRb\implies bRa)$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Asimétrica: -\series default - -\begin_inset Formula $\forall a,b\in A,(aRb\implies b\not Ra)$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Antisimétrica: -\series default - -\begin_inset Formula $\forall a,b\in A,(aRb\land bRa\implies a=b)$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Transitiva: -\series default - -\begin_inset Formula $\forall a,b,c\in A,(aRb\land bRc\implies aRc)$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Intransitiva: -\series default - -\begin_inset Formula $\forall a,b,c\in A,(aRb\land bRc\implies a\not Rc)$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Negativamente transitiva: -\series default - -\begin_inset Formula $\forall a,b,c\in A,(a\not Rb\land b\not Rc\implies a\not Rc)$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Completa: -\series default - -\begin_inset Formula $\forall a,b\in A,(aRb\lor bRa)$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Euclídea: -\series default - -\begin_inset Formula $\forall a,b,c\in A,(aRb\land aRc\implies bRc)$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Incestuosa: -\series default - -\begin_inset Formula $\forall a,b,c\in A,(aRb\land aRc\implies\exists d\in A:(bRd\land cRd))$ -\end_inset - -. -\end_layout - -\begin_layout Plain Layout -Dada -\begin_inset Formula $R\subseteq A\times B$ -\end_inset - -, su -\series bold -relación inversa -\series default - es -\begin_inset Formula $R^{-1}$ -\end_inset - - con -\begin_inset Formula $xR^{-1}y:\iff yRx$ -\end_inset - -. - Dada -\begin_inset Formula $R\subseteq A\times A$ -\end_inset - -: -\end_layout - -\begin_layout Itemize -Su -\series bold -relación complementaria -\series default - es -\begin_inset Formula $R^{\complement}$ -\end_inset - - con -\begin_inset Formula $xR^{\complement}y:\iff x\not Ry$ -\end_inset - -. -\end_layout - -\begin_layout Itemize -Su -\series bold -relación simétrica -\series default - es -\begin_inset Formula $\overline{R}=R^{-1}$ -\end_inset - - con -\begin_inset Formula $x\overline{R}y:\iff yRx$ -\end_inset - -. -\end_layout - -\begin_layout Itemize -Su -\series bold -relación dual -\series default - es -\begin_inset Formula $R^{d}$ -\end_inset - - con -\begin_inset Formula $aR^{d}b:\iff b\not Ra$ -\end_inset - -. -\end_layout - -\begin_layout Plain Layout -Una relación de equivalencia es aquella reflexiva, simétrica y transitiva. - Sea -\begin_inset Formula $(A,\sim)$ -\end_inset - - de equivalencia, podemos definir la clase de equivalencia de -\begin_inset Formula $x$ -\end_inset - -, -\begin_inset Formula $[x]$ -\end_inset - -, como el conjunto de todos los elementos que se relacionan con -\begin_inset Formula $[x]$ -\end_inset - -. - -\begin_inset Formula $y\in[x]\implies[y]=[x]$ -\end_inset - -, y decimos que -\begin_inset Formula $y$ -\end_inset - - es un representante de la clase. - El conjunto cociente es el formado por todas las clases de equivalencia, - y se escribe -\begin_inset Formula $A/\sim=\{[x]|x\in A\}$ -\end_inset - -. -\end_layout - -\end_inset - - -\end_layout - -\begin_layout Section -Sintaxis -\end_layout - -\begin_layout Itemize - -\series bold -Proposición atómica: -\series default - -\begin_inset Formula $V$ -\end_inset - -, -\begin_inset Formula $F$ -\end_inset - - o un predicado. -\end_layout - -\begin_layout Itemize - -\series bold -Predicado: -\series default - Secuencia de letras latinas que representa una relación, seguida de una - serie de términos: -\begin_inset Formula $R(t_{1},\dots,t_{n})$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Término: -\series default - Constante que representa un objeto definido, variable o función. -\end_layout - -\begin_layout Itemize - -\series bold -Constante: -\series default - Secuencia de letras latinas que representa a un objeto definido (salvo - -\begin_inset Formula $V$ -\end_inset - - y -\begin_inset Formula $F$ -\end_inset - -). -\end_layout - -\begin_layout Itemize - -\series bold -Variable: -\series default - Secuencia de letras latinas que representa a un objeto indefinido. - Puede estar -\series bold -ligada -\series default - a un cuantificador, y entonces es igual al resto de variables ligadas al - mismo, o -\series bold -libre -\series default -, en cuyo caso puede representar cualquier cosa. -\end_layout - -\begin_layout Itemize - -\series bold -Función: -\series default - Secuencia de letras latinas que representa una función, seguida de una - serie de términos: -\begin_inset Formula $f(t_{1},\dots,t_{n})$ -\end_inset - -. -\end_layout - -\begin_layout Standard -La construcción de f.b.f es igual que en L0, pero cambiando la forma de las - proposiciones atómicas y añadiendo que si -\begin_inset Formula $\alpha$ -\end_inset - - es f.b.f. - también lo son -\begin_inset Formula $(\forall x\alpha)$ -\end_inset - - y -\begin_inset Formula $(\exists x\alpha)$ -\end_inset - -. - Una f.b.f. - es -\series bold -cerrada -\series default - si todas las variables están ligadas y -\series bold -abierta -\series default - en otro caso. -\end_layout - -\begin_layout Section -Interpretación y asignación -\end_layout - -\begin_layout Standard -Una -\series bold -interpretación -\series default - de -\begin_inset Formula $\alpha$ -\end_inset - - en un -\series bold -mundo -\series default - -\begin_inset Formula $\mathbb{M}$ -\end_inset - - es una cuaterna -\begin_inset Formula ${\cal I}_{\alpha}=(\mathbb{D},{\cal C}_{\mathbb{D}},{\cal F}_{\mathbb{D}},{\cal R}_{\mathbb{D}})$ -\end_inset - - donde -\begin_inset Formula $\mathbb{D}$ -\end_inset - - es un conjunto no vacío de objetos, llamado dominio, -\begin_inset Formula ${\cal C}_{\mathbb{D}}$ -\end_inset - - es un conjunto de objetos concretos ( -\begin_inset Formula ${\cal C_{\alpha}\mapsto{\cal C}_{\mathbb{D}}}$ -\end_inset - -), -\begin_inset Formula ${\cal F}_{\mathbb{D}}$ -\end_inset - - de funciones concretas ( -\begin_inset Formula $f_{\alpha}\mapsto f_{\mathbb{D}}$ -\end_inset - -) y -\begin_inset Formula ${\cal R}_{\mathbb{D}}$ -\end_inset - - de relaciones concretas ( -\begin_inset Formula $R_{\alpha}\mapsto R_{\mathbb{D}}$ -\end_inset - -). - La -\series bold -signatura -\series default - es el conjunto de todos los predicados y funciones, indicando su aridad. -\end_layout - -\begin_layout Standard -Una asignación de variables es una función -\begin_inset Formula $\sigma_{{\cal I}_{\alpha}}:{\cal V}\rightarrow\mathbb{D}$ -\end_inset - - que relaciona cada variable de -\begin_inset Formula $\alpha$ -\end_inset - - con un elemento del dominio, y definimos -\begin_inset Formula $\sigma_{{\cal I}_{\alpha}|x\looparrowright d}$ -\end_inset - - a la asignación definida igual que -\begin_inset Formula $\sigma_{{\cal I}_{\alpha}}$ -\end_inset - - pero asignando a -\begin_inset Formula $x$ -\end_inset - - el objeto -\begin_inset Formula $d$ -\end_inset - -. -\end_layout - -\begin_layout Standard -Una -\series bold -asignación de valores de verdad -\series default - -\begin_inset Formula $v_{\sigma_{{\cal I}_{\alpha}}}:{\cal P_{\alpha}\rightarrow\mathbb{B}}$ -\end_inset - - asigna un valor de verdad a cada elemento atómico de -\begin_inset Formula $\alpha$ -\end_inset - -. - Así, -\begin_inset Formula $v(R_{\alpha}(t_{1},\dots,t_{n}))=V\iff(d_{1},\dots,d_{n})\in R_{\mathbb{D}}$ -\end_inset - -, donde si -\begin_inset Formula $t_{i}$ -\end_inset - - es constante entonces -\begin_inset Formula $d_{i}=t_{i}$ -\end_inset - -, si -\begin_inset Formula $t_{i}=f(x_{1},\dots,x_{n})$ -\end_inset - - entonces -\begin_inset Formula $d_{i}$ -\end_inset - - es el único -\begin_inset Formula $y$ -\end_inset - - tal que -\begin_inset Formula $(x_{1},\dots,x_{n},y)\in f$ -\end_inset - -, y si es variable entonces depende de la -\series bold -asignación -\series default -. -\end_layout - -\begin_layout Standard -La -\series bold -evaluación -\series default - de una oración -\begin_inset Formula $\alpha$ -\end_inset - - se hace igual que en LC, pero partiendo de esta asignación de valores de - verdad. - También se puede hacer mediante tablas de verdad, que en L1 sólo evalúan - una interpretación a la vez: -\end_layout - -\begin_layout Enumerate -Se introduce una columna por variable, dividida en una fila por cada valor - del dominio. - Puede ser necesario considerar aquí todas las posibles combinaciones de - variables. -\end_layout - -\begin_layout Enumerate -Se introduce una columna por cada función que aparece en la oración, y se - evalúa de acuerdo al valor de la variable dado. -\end_layout - -\begin_layout Enumerate -Se introducen las filas correspondientes a la fórmula, indicando el orden - de evaluación. - Un cuantificador que no está dentro de otro ocupa la fila completa, pero - su contenido se divide en una fila por cada posible asignación de la variable. - Una vez se conoce el valor del cuantificador no es necesario evaluar el - resto de asignaciones, pero es importante justificar los valores de verdad - de los predicados (ejemplos: -\begin_inset Formula $V:(a,b)\in P_{{\cal M}}$ -\end_inset - -; -\begin_inset Formula $F:(c,a)\notin Q_{{\cal M}}$ -\end_inset - -). -\end_layout - -\begin_layout Standard -Este método es impráctico, por lo que no se usa. -\end_layout - -\begin_layout Section -Sustituciones -\end_layout - -\begin_layout Standard -Una -\series bold -sustitución -\series default - es una expresión -\begin_inset Formula $s=\{t_{1}/v_{1},\dots,t_{n}/v_{n}\}$ -\end_inset - - que indica que toda ocurrencia de cada -\begin_inset Formula $v_{i}$ -\end_inset - - se debe sustituir por el término -\begin_inset Formula $t_{i}$ -\end_inset - -. - Todas las sustituciones se hacen simultáneamente. -\end_layout - -\begin_layout Standard -Una -\series bold -particularización por sustitución -\series default - consiste en sustituir sus variables por términos. - Escribimos -\begin_inset Formula $Ps$ -\end_inset - - como la particularización de la expresión -\begin_inset Formula $P$ -\end_inset - - según la sustitución -\begin_inset Formula $s$ -\end_inset - -. -\end_layout - -\begin_layout Itemize -En una -\series bold -particularización básica -\series default -, los términos son constantes. -\end_layout - -\begin_layout Itemize -En una -\series bold -particularización alfabética -\series default -, los términos son otras variables. -\end_layout - -\begin_layout Standard - -\series bold -Composición de sustituciones: -\series default - Dadas -\begin_inset Formula $s=\{a_{1}/x_{1},\dots,a_{n}/x_{n}\}$ -\end_inset - - y -\begin_inset Formula $t=\{b_{1}/y_{1},\dots,b_{m}/y_{m}\}$ -\end_inset - - con -\begin_inset Formula $X$ -\end_inset - - e -\begin_inset Formula $Y$ -\end_inset - - los conjuntos de variables sustituidas respectivamente según -\begin_inset Formula $s$ -\end_inset - - y -\begin_inset Formula $t$ -\end_inset - -, -\begin_inset Formula $s\cdot t=\{(a_{i}t)/x_{i}|x_{i}\neq a_{i}t\}\cup\{b_{i}/y_{i}|y_{i}\in Y\backslash X\}$ -\end_inset - -, donde -\begin_inset Formula $a_{i}t$ -\end_inset - - es la particularización de -\begin_inset Formula $a_{i}$ -\end_inset - - según -\begin_inset Formula $t$ -\end_inset - -. -\end_layout - -\begin_layout Section -Equivalencias -\end_layout - -\begin_layout Standard -\align center -\begin_inset Tabular - - - - - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\neg\exists x\alpha[x]\equiv\forall x\neg\alpha[x]$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\neg\forall x\alpha[x]\equiv\exists x\neg\alpha[x]$ -\end_inset - - -\end_layout - -\end_inset - - - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\forall x(\alpha[x]\land\beta[x])\equiv\forall x\alpha[x]\land\forall x\beta[x]$ -\end_inset - - -\end_layout - -\end_inset - - -\begin_inset Text - -\begin_layout Plain Layout -\begin_inset Formula $\exists x(\alpha[x]\lor\beta[x])\equiv\exists x\alpha[x]\lor\exists x\beta[x]$ -\end_inset - - -\end_layout - -\end_inset - - - - -\end_inset - - -\end_layout - -\begin_layout Standard -También, tanto en L1 como en LC, podemos sustituir el nombre de una variable - por otro siempre que lo cambiemos en el cuantificador al que está ligado - y en todos los símbolos ligados al mismo cuantificador (o bien la variable - sea libre), y al hacerlo todas las variables de la oración sigan ligadas - al mismo cuantificador de partida (o sigan libres). -\end_layout - -\begin_layout Section -Satisfacibilidad -\end_layout - -\begin_layout Standard -Podemos comprobar la satisfacibilidad de una oración mediante tableaux. - Añadimos dos tipos de reglas: -\end_layout - -\begin_layout Itemize -\begin_inset Formula $\gamma$ -\end_inset - - -\series bold --reglas -\series default -: -\begin_inset Formula $\forall x\alpha[x]\mapsto\alpha[C],\forall x\alpha[x]$ -\end_inset - -; -\begin_inset Formula $\neg\exists x\alpha[x]\mapsto\neg\alpha[C],\neg\exists x\alpha[x]$ -\end_inset - -. - La sustitución -\begin_inset Formula $\{C/x\}$ -\end_inset - - se hace sobre una constante -\begin_inset Formula $C$ -\end_inset - - existente. - Si no existe ninguna, debemos suponer una nueva. - El -\begin_inset Formula $\forall x\alpha[x]$ -\end_inset - - resultante no hace referencia a -\begin_inset Formula $C$ -\end_inset - -, de modo que se debe escribir una lista debajo de cada expresión de este - tipo ( -\begin_inset Formula $L=\{\dots\}$ -\end_inset - -) con los elementos a los que sí hace referencia. -\end_layout - -\begin_layout Itemize -\begin_inset Formula $\delta$ -\end_inset - - -\series bold --reglas -\series default -: -\begin_inset Formula $\exists x\alpha[x]\mapsto\alpha[C]$ -\end_inset - -; -\begin_inset Formula $\neg\forall x\alpha[x]\mapsto\neg\alpha[C]$ -\end_inset - -. - La sustitución -\begin_inset Formula $\{C/x\}$ -\end_inset - - se hace sobre una constante -\begin_inset Formula $C$ -\end_inset - - nueva, y entonces se debe añadir a las listas de todas las expresiones - de -\begin_inset Formula $\gamma$ -\end_inset - --reglas dicha constante. -\end_layout - -\begin_layout Standard -Al aplicar estas reglas, se debe indicar, por ejemplo: -\begin_inset Formula $\gamma:\forall x;\{C/x\};C\text{ nueva}$ -\end_inset - - (la última parte se incluye siempre en las -\begin_inset Formula $\delta$ -\end_inset - --reglas). - Las -\begin_inset Formula $\delta$ -\end_inset - --reglas se aplican después de las -\begin_inset Formula $\beta$ -\end_inset - --reglas y antes de las -\begin_inset Formula $\gamma$ -\end_inset - --reglas, y si se llega a un bucle por una rama, se razona que el tableaux - es abierto. -\end_layout - -\begin_layout Standard -Si el tableaux es cerrado (si todas las hojas están cerradas), llegamos - a una contradicción. - Sin embargo, si el tableaux es abierto, no sabemos que sea satisfacible - (salvo si todos los predicados son de aridad 1 o la identidad). - No obstante, los nodos abiertos pueden servir como ejemplos de interpretaciones - en las que la oración es satisfacible. -\end_layout - -\begin_layout Section -Grafos semánticos -\end_layout - -\begin_layout Standard -Son iguales que en L0, pero en los cuantificadores, el nombre de la variable - se incluye en el nombre del propio nodo junto con el cuantificador. - Además, debajo de cada predicado (que se escribe completo), se puede indicar - el f.b.f. - de términos, que consiste en añadir un nodo hijo por cada término. - Si el término es una función, se indica simplemente el nombre de la función - y sus parámetros se escriben como nodos hijo. -\end_layout - -\begin_layout Section -Deducción natural -\end_layout - -\begin_layout Standard -Se añaden reglas de deducción natural: -\end_layout - -\begin_layout Itemize -\begin_inset Formula $E_{\forall}:\frac{\vdash\forall x\alpha[x]}{\vdash\alpha[C]}$ -\end_inset - -. - -\begin_inset Formula $C$ -\end_inset - - es una constante cualquiera. - Se debe indicar la sustitución -\begin_inset Formula $\{C/x\}$ -\end_inset - - y, en su caso, si -\begin_inset Formula $C$ -\end_inset - - es nueva o -\begin_inset Quotes cld -\end_inset - -arbitraria -\begin_inset Quotes crd -\end_inset - -. -\end_layout - -\begin_layout Itemize -\begin_inset Formula $I_{\forall}:\frac{\vdash\alpha[C]}{\vdash\forall x\alpha[x]}$ -\end_inset - -. - -\begin_inset Formula $C$ -\end_inset - - debe ser -\begin_inset Quotes cld -\end_inset - -arbitraria -\begin_inset Quotes crd -\end_inset - -, es decir, no distinguible de cualquier otro individuo por suposiciones, - derivaciones o premisas anteriores. - Puede ser obtenida nueva con -\begin_inset Formula $E_{\forall}$ -\end_inset - -. -\end_layout - -\begin_layout Itemize -\begin_inset Formula $E_{\exists}:\frac{\vdash\exists x\alpha[x]\vdash(\alpha[C]\vdash\beta)}{\vdash\beta}$ -\end_inset - -. - No se debe hacer ninguna suposición sobre -\begin_inset Formula $C$ -\end_inset - -, y -\begin_inset Formula $\beta$ -\end_inset - - no puede depender de -\begin_inset Formula $C$ -\end_inset - -. -\end_layout - -\begin_layout Itemize -\begin_inset Formula $I_{\exists}:\frac{\vdash\alpha[C]}{\vdash\exists x\alpha[x]}$ -\end_inset - -. - Se pueden cambiar todas las apariciones de -\begin_inset Formula $C$ -\end_inset - - o solo algunas. -\end_layout - -\end_body -\end_document diff --git a/logic/n7.lyx b/logic/n7.lyx deleted file mode 100644 index b05b04e..0000000 --- a/logic/n7.lyx +++ /dev/null @@ -1,609 +0,0 @@ -#LyX 2.3 created this file. For more info see http://www.lyx.org/ -\lyxformat 544 -\begin_document -\begin_header -\save_transient_properties true -\origin unavailable -\textclass book -\use_default_options true -\maintain_unincluded_children false -\language spanish -\language_package default -\inputencoding auto -\fontencoding global -\font_roman "default" "default" -\font_sans "default" "default" -\font_typewriter "default" "default" -\font_math "auto" "auto" -\font_default_family default -\use_non_tex_fonts false -\font_sc false -\font_osf false -\font_sf_scale 100 100 -\font_tt_scale 100 100 -\use_microtype false -\use_dash_ligatures true -\graphics default -\default_output_format default -\output_sync 0 -\bibtex_command default -\index_command default -\paperfontsize default -\spacing single -\use_hyperref false -\papersize default -\use_geometry false -\use_package amsmath 1 -\use_package amssymb 1 -\use_package cancel 1 -\use_package esint 1 -\use_package mathdots 1 -\use_package mathtools 1 -\use_package mhchem 1 -\use_package stackrel 1 -\use_package stmaryrd 1 -\use_package undertilde 1 -\cite_engine basic -\cite_engine_type default -\biblio_style plain -\use_bibtopic false -\use_indices false -\paperorientation portrait -\suppress_date false -\justification true -\use_refstyle 1 -\use_minted 0 -\index Index -\shortcut idx -\color #008000 -\end_index -\secnumdepth 3 -\tocdepth 3 -\paragraph_separation indent -\paragraph_indentation default -\is_math_indent 0 -\math_numbering_side default -\quotes_style swiss -\dynamic_quotes 0 -\papercolumns 1 -\papersides 1 -\paperpagestyle default -\tracking_changes false -\output_changes false -\html_math_output 0 -\html_css_as_file 0 -\html_be_strict false -\end_header - -\begin_body - -\begin_layout Standard -Un -\series bold -sistema deductivo -\series default - es un conjunto de axiomas y reglas de inferencia sintácticas ( -\begin_inset Formula $\vdash$ -\end_inset - -). - Una -\series bold -demostración -\series default - o -\series bold -prueba formal -\series default - es una secuencia de conjuntos de fórmulas en las que cada fórmula es un - axioma o puede obtenerse del conjunto anterior mediante una regla de inferencia. - Cada elemento -\begin_inset Formula $\alpha$ -\end_inset - - del último conjunto de la secuencia se llama -\series bold -teorema por deducción -\series default -, y se dice que -\begin_inset Formula $\alpha$ -\end_inset - - es -\series bold -demostrable -\series default -, lo que escribimos como -\begin_inset Formula $\vdash\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Standard -Un sistema deductivo en L0 y L1 es -\series bold -sólido -\series default - si y sólo si -\begin_inset Formula $\vdash\alpha\implies\vDash\alpha$ -\end_inset - -, es decir, si cualquier conclusión -\series bold -derivable -\series default - o -\series bold -deducible -\series default -a partir de las reglas es válida, y es -\series bold -completo -\series default - cuando -\begin_inset Formula $\vDash\alpha\implies\vdash\alpha$ -\end_inset - -. - Un conjunto de reglas es -\series bold -inconsistente -\series default - si -\begin_inset Formula $\vdash\alpha\land\neg\alpha$ -\end_inset - -, y es -\series bold -consistente -\series default - si no es inconsistente. -\end_layout - -\begin_layout Standard -Dada una oración -\begin_inset Formula $\alpha$ -\end_inset - - y un conjunto de oraciones -\begin_inset Formula ${\cal F}$ -\end_inset - -, -\begin_inset Formula $\vDash\alpha$ -\end_inset - - significa que -\begin_inset Formula $\alpha$ -\end_inset - - es válida y -\begin_inset Formula ${\cal F}\vDash\alpha$ -\end_inset - - significa que -\begin_inset Formula $\alpha$ -\end_inset - - es consecuencia lógica de -\begin_inset Formula ${\cal F}$ -\end_inset - -. - Por su parte -\begin_inset Formula $\vdash\alpha$ -\end_inset - - significa que -\begin_inset Formula $\alpha$ -\end_inset - - es demostrable y -\begin_inset Formula ${\cal F}\vdash\alpha$ -\end_inset - - significa que -\begin_inset Formula $\alpha$ -\end_inset - - es deducible de -\begin_inset Formula ${\cal F}$ -\end_inset - -, y representa una -\series bold -deducción -\series default - o -\series bold -razonamiento -\series default -, donde -\begin_inset Formula $\alpha$ -\end_inset - - es la conclusión o -\series bold -derivación -\series default - y las -\begin_inset Formula $\psi\in{\cal F}$ -\end_inset - - son las premisas, las fórmulas usadas para llegar a -\begin_inset Formula $\alpha$ -\end_inset - -. - -\end_layout - -\begin_layout Standard -Decimos que un conjunto de oraciones -\begin_inset Formula ${\cal T}$ -\end_inset - - es una -\series bold -teoría -\series default - si -\begin_inset Formula $\forall\alpha({\cal T}\vDash\alpha\implies\alpha\in{\cal T})$ -\end_inset - -, y entonces cada -\begin_inset Formula $\alpha\in{\cal T}$ -\end_inset - - es un -\series bold -teorema -\series default -. - Una teoría es -\series bold -axiomatizable -\series default - si existe un subconjunto -\begin_inset Formula ${\cal F}$ -\end_inset - - tal que -\begin_inset Formula ${\cal T}=\{\alpha|{\cal F}\vDash\alpha\}$ -\end_inset - -, y cada -\begin_inset Formula $\alpha\in{\cal F}$ -\end_inset - - es un -\series bold -axioma -\series default -, y es -\series bold -contradictoria -\series default - o -\series bold -inconsistente -\series default - cuando -\begin_inset Formula ${\cal T}\vDash\alpha$ -\end_inset - - y -\begin_inset Formula ${\cal T}\vDash\neg\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Standard -Una teoría es -\series bold -decidible -\series default - si se puede determinar la consistencia o inconsistencia de una fórmula - mediante un algoritmo; -\series bold -semidecidible -\series default - si hay fórmulas cuya inconsistencia no puede ser probada algorítmicamente, - e -\series bold -indecidible -\series default - si no es posible crear un algoritmo que determine la consistencia o inconsisten -cia de una fórmula. -\end_layout - -\begin_layout Standard - -\series bold -Hilbert -\series default - opinaba que todo sistema fundamental matemático debía ser consistente, - completo y decidible, pero Kurt -\series bold - Gödel -\series default - demostró que ningún sistema capaz de representar los números naturales - puede ser a la vez consistente y completo, y que la consistencia no puede - probarse con los propios axiomas del sistema, por lo que habrá verdades - que no se pueden demostrar. - Alan -\series bold -Turing -\series default -, por su parte, demostró que solo sistemas muy restrictivos son decidibles. -\end_layout - -\begin_layout Standard -Un sistema deductivo cumple el -\series bold -teorema de la deducción -\series default - si verifica que, dado el conjunto -\begin_inset Formula ${\cal F}$ -\end_inset - - y las fórmulas -\begin_inset Formula $\alpha$ -\end_inset - - y -\begin_inset Formula $\beta$ -\end_inset - -, -\begin_inset Formula ${\cal F}\cup\{\alpha\}\vdash\beta\iff{\cal F}\vdash\alpha\rightarrow\beta$ -\end_inset - -. - Así, -\begin_inset Formula ${\cal F}\cup\{\alpha_{1},\dots,\alpha_{n}\}\vdash\beta\iff{\cal F}\cup\{\alpha_{1},\dots,\alpha_{n-1}\}\vdash\alpha_{n}\rightarrow\beta\iff\dots\iff{\cal F}\vdash\alpha_{1}\rightarrow(\alpha_{2}\rightarrow\cdots(\alpha_{n}\rightarrow\beta)\cdots)$ -\end_inset - -. - Este teorema simplifica mucho las demostraciones, si bien no se probó su - corrección hasta 1930. - No todos los sistemas cumplen en teorema de la deducción, si bien el Teorema - de la Deducción Semántica ( -\begin_inset Formula ${\cal F}\cup\{a\}\vDash\beta\iff{\cal F}\vDash\alpha\rightarrow\beta$ -\end_inset - -) se cumple siempre. - Decimos que -\begin_inset Formula ${\cal F}$ -\end_inset - - es -\series bold -sintácticamente completo -\series default - si para todo -\begin_inset Formula $\alpha$ -\end_inset - -, -\begin_inset Formula ${\cal F}\vdash\alpha$ -\end_inset - - o -\begin_inset Formula ${\cal F}\vdash\neg\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Standard -Un -\series bold -razonamiento deductivo -\series default - es el que parte de unas hipótesis básicas para obtener unas consecuencias - ( -\begin_inset Formula $\alpha\vDash\beta$ -\end_inset - -). - Normalmente parte de premisas sobre aspectos generales para concluir aspectos - particulares. - La relación entre premisas y conclusión es de implicación ( -\begin_inset Formula $\alpha\vDash\beta\iff\vDash\alpha\rightarrow\beta$ -\end_inset - -). - Algunos tipos de -\series bold -demostración -\series default - deductiva (de -\begin_inset Formula $\vDash\alpha\rightarrow\beta$ -\end_inset - -): -\end_layout - -\begin_layout Itemize - -\series bold -Vacía -\series default - de -\begin_inset Formula $\alpha\rightarrow\beta$ -\end_inset - -: -\begin_inset Formula $\forall v_{I},v(\alpha)=F$ -\end_inset - - (no se usa -\begin_inset Formula $\beta$ -\end_inset - -). -\end_layout - -\begin_layout Itemize - -\series bold -Trivial -\series default -: -\begin_inset Formula $\forall v_{I},v(\beta)=V$ -\end_inset - - (no se usa -\begin_inset Formula $\alpha$ -\end_inset - -). -\end_layout - -\begin_layout Itemize - -\series bold -Directa -\series default -: Probar que -\begin_inset Formula $\alpha\vDash\beta$ -\end_inset - - usando definiciones o teoremas ya probados, como el Modus Ponens. -\end_layout - -\begin_layout Itemize - -\series bold -Por contrarrecíproco -\series default -: -\begin_inset Formula $\alpha\rightarrow\beta\equiv\neg\beta\rightarrow\neg\alpha$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Por contradicción -\series default -: -\begin_inset Formula $\alpha\rightarrow\beta\equiv\alpha\land\neg\beta\rightarrow\gamma\land\neg\gamma$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Indirecta -\series default -: Si -\begin_inset Formula $\alpha\vDash\gamma$ -\end_inset - - y -\begin_inset Formula $\gamma\vDash\beta$ -\end_inset - - entonces -\begin_inset Formula $\alpha\vDash\beta$ -\end_inset - -. -\end_layout - -\begin_layout Standard -La -\series bold -refutación por contraejemplo -\series default - consiste en buscar -\begin_inset Formula $a$ -\end_inset - - tal que -\begin_inset Formula $v(\alpha[a]\rightarrow\beta[a])=F$ -\end_inset - -. -\end_layout - -\begin_layout Standard -Un -\series bold -razonamiento inductivo -\series default - consiste en obtener reglas generales a partir de casos particulares. - Para ello se observan, registran y analizan hechos y se formulan leyes - universales a modo de hipótesis o conjeturas, tras lo cual se diseñan experimen -tos para ver que estas leyes se cumplen. -\end_layout - -\begin_layout Standard -La -\series bold -inducción matemática -\series default -, sin embargo, se puede probar de forma deductiva, si bien esto requiere - lógica de segundo orden. - En -\begin_inset Formula $\mathbb{N}$ -\end_inset - -, para un -\begin_inset Formula $n_{0}\in\mathbb{N}$ -\end_inset - -, tenemos: -\end_layout - -\begin_layout Itemize - -\series bold -Principio de inducción débil -\series default -: -\begin_inset Formula $\{P(n_{0})\}\cup\bigcup_{n\geq n_{0}}\{P(n)\rightarrow P(n+1)\}\vDash\forall n\geq n_{0},P(n)$ -\end_inset - -. -\end_layout - -\begin_layout Itemize - -\series bold -Principio de inducción fuerte -\series default -: -\begin_inset Formula $\{P(n_{0})\}\cup\bigcup_{n\geq n_{0}}\{P(n_{0})\land\dots\land P(n)\rightarrow P(n+1)\}\vDash\forall n\geq n_{0},P(n)$ -\end_inset - -. -\end_layout - -\begin_layout Standard -El -\series bold -principio de inducción estructural -\series default - para -\series bold -demostración por recursión -\series default - es una generalización de la inducción y afirma que, dado un conjunto de - elementos definido por recursión con una serie de casos base y reglas de - recursión sobre estos, si una propiedad se cumple para cada caso base, - y si en cada regla de recursión si la propiedad se cumple para los parámetros - de entrada también se cumple para el elemento resultante de aplicarla, - entonces esta propiedad la cumplen todos los elementos del conjunto. -\end_layout - -\end_body -\end_document diff --git a/si/n3.lyx b/si/n3.lyx index 06957fb..91b18ae 100644 --- a/si/n3.lyx +++ b/si/n3.lyx @@ -1837,7 +1837,7 @@ SetKwFunction{Resolucion}{{}resolución} \begin_layout Plain Layout -$R +$G \backslash gets \backslash @@ -1845,7 +1845,7 @@ gets \backslash }$ \backslash -tcp*{Por resolver} +tcp*{Generados} \end_layout \begin_layout Plain Layout @@ -1925,13 +1925,15 @@ leq F$}{ Tomar $n \backslash -in R +in G \backslash setminus \backslash text{Dom}b$ \backslash -; +tcp*{{ +\backslash +rm Esta es la frontera.}} \end_layout \begin_layout Plain Layout @@ -1966,7 +1968,7 @@ emptyset$}{ $w_n \backslash -gets F$ +gets 0$ \backslash ; \end_layout @@ -2029,7 +2031,7 @@ gets0$ \backslash EnOtroCasoSi{$u \backslash -notin R$}{ +notin G$}{ \end_layout \begin_layout Plain Layout @@ -2048,7 +2050,7 @@ gets h(u)$ \begin_layout Plain Layout - Añadir $u$ a $R$ + Añadir $u$ a $G$ \backslash ; \end_layout @@ -2096,6 +2098,19 @@ in M$ sin sucesores en $M$ y sacarlo de $M$ ; \end_layout +\begin_layout Plain Layout + + $c +\backslash +gets(w_u,[u +\backslash +in C])$ +\backslash +tcp*{{ +\backslash +rm $[P]$ devuelve un booleano que indica si $P$ es cierto.}} +\end_layout + \begin_layout Plain Layout Tomar el $S$ con $(u,S) @@ -2146,15 +2161,29 @@ subseteq C$}{añadir $u$ a $C$} \begin_layout Plain Layout - Añadir a $M$ los $v + +\backslash +lSSi{$c +\backslash +neq(w_u,[u +\backslash +in C])$}{% +\end_layout + +\begin_layout Plain Layout + + añadir a $M$ los $v \backslash in \backslash text{Dom}b$ con $u \backslash -in b_v$ -\backslash -; +in b_v$% +\end_layout + +\begin_layout Plain Layout + + } \end_layout \begin_layout Plain Layout -- cgit v1.2.3