diff options
Diffstat (limited to 'fli')
| -rw-r--r-- | fli/n.lyx | 253 | ||||
| -rw-r--r-- | fli/n1.lyx | 346 | ||||
| -rw-r--r-- | fli/n2.lyx | 1518 | ||||
| -rw-r--r-- | fli/n3.lyx | 1512 | ||||
| -rw-r--r-- | fli/n4.lyx | 402 | ||||
| -rw-r--r-- | fli/n5.lyx | 660 | ||||
| -rw-r--r-- | fli/n6.lyx | 1406 | ||||
| -rw-r--r-- | fli/n7.lyx | 609 |
8 files changed, 6706 insertions, 0 deletions
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 +<lyxtabular version="3" rows="7" columns="6"> +<features tabularvalignment="middle"> +<column alignment="center" valignment="top"> +<column alignment="center" valignment="top"> +<column alignment="center" valignment="top"> +<column alignment="center" valignment="top"> +<column alignment="center" valignment="top"> +<column alignment="center" valignment="top"> +<row> +<cell multicolumn="1" alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha$ +\end_inset + +-fórmulas +\end_layout + +\end_inset +</cell> +<cell multicolumn="2" alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset +</cell> +<cell multicolumn="2" alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset +</cell> +<cell multicolumn="1" alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\beta$ +\end_inset + +-fórmulas +\end_layout + +\end_inset +</cell> +<cell multicolumn="2" alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset +</cell> +<cell multicolumn="2" alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset +</cell> +</row> +<row> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha_{1}$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha_{2}$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\beta$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\beta_{1}$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\beta_{2}$ +\end_inset + + +\end_layout + +\end_inset +</cell> +</row> +<row> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg\neg\alpha$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset +</cell> +</row> +<row> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha\land\beta$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\beta$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg(\alpha\land\beta)$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg\alpha$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg\beta$ +\end_inset + + +\end_layout + +\end_inset +</cell> +</row> +<row> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg(\alpha\lor\beta)$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg\alpha$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg\beta$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha\lor\beta$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\beta$ +\end_inset + + +\end_layout + +\end_inset +</cell> +</row> +<row> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg(\alpha\rightarrow\beta)$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg\beta$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha\rightarrow\beta$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg\alpha$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\beta$ +\end_inset + + +\end_layout + +\end_inset +</cell> +</row> +<row> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha\leftrightarrow\beta$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\alpha\rightarrow\beta$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\beta\rightarrow\alpha$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg(\alpha\leftrightarrow\beta)$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg(\alpha\rightarrow\beta)$ +\end_inset + + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +\begin_inset Formula $\neg(\beta\rightarrow\alpha)$ +\end_inset + + +\end_layout + +\end_inset +</cell> +</row> +</lyxtabular> + +\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 +<lyxtabular version="3" rows="8" columns="3"> +<features tabularvalignment="middle"> +<column alignment="center" valignment="top"> +<column alignment="center" valignment="top"> +<column alignment="center" valignment="top"> +<row> +<cell alignment="center" valignment="top" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +Eliminación de +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +Introducción de +\end_layout + +\end_inset +</cell> +</row> +<row> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +la conjunción +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\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 +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none"> +\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 +</cell> +</row> +<row> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +la disyunción +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\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 +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none"> +\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 +</cell> +</row> +<row> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +la implicación +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\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 +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none"> +\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 +</cell> +</row> +<row> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +la doble implicación +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\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 +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none"> +\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 +</cell> +</row> +<row> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +la negación +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\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 +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none"> +\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 +</cell> +</row> +<row> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +la doble negación +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\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 +</cell> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset +</cell> +</row> +<row> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout +la contradicción +\end_layout + +\end_inset +</cell> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none"> +\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 +</cell> +<cell alignment="center" valignment="top" leftline="true" usebox="none"> +\begin_inset Text + +\begin_layout Plain Layout + +\end_layout + +\end_inset +</cell> +</row> +</lyxtabular> + +\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 +<lyxtabular version="3" rows="2" columns="2"> +<features tabularvalignment="middle"> +<column alignment="center" valignment="top"> +<column alignment="center" valignment="top"> +<row> +<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none"> +\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 +</cell> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none"> +\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 +</cell> +</row> +<row> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none"> +\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 +</cell> +<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none"> +\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 +</cell> +</row> +</lyxtabular> + +\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 |