Actualizado README

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