Actualizado README

8 files changed, 0 insertions, 6706 deletions

diff --git a/logic/n.lyx b/logic/n.lyx
deleted file mode 100644
index 57fe1dd..0000000
--- a/logic/n.lyx
+++ /dev/null
@@ -1,253 +0,0 @@
-#LyX 2.3 created this file. For more info see http://www.lyx.org/
-\lyxformat 544
-\begin_document
-\begin_header
-\save_transient_properties true
-\origin unavailable
-\textclass book
-\use_default_options true
-\maintain_unincluded_children false
-\language spanish
-\language_package default
-\inputencoding auto
-\fontencoding global
-\font_roman "default" "default"
-\font_sans "default" "default"
-\font_typewriter "default" "default"
-\font_math "auto" "auto"
-\font_default_family default
-\use_non_tex_fonts false
-\font_sc false
-\font_osf false
-\font_sf_scale 100 100
-\font_tt_scale 100 100
-\use_microtype false
-\use_dash_ligatures true
-\graphics default
-\default_output_format default
-\output_sync 0
-\bibtex_command default
-\index_command default
-\paperfontsize default
-\spacing single
-\use_hyperref false
-\papersize a5paper
-\use_geometry true
-\use_package amsmath 1
-\use_package amssymb 1
-\use_package cancel 1
-\use_package esint 1
-\use_package mathdots 1
-\use_package mathtools 1
-\use_package mhchem 1
-\use_package stackrel 1
-\use_package stmaryrd 1
-\use_package undertilde 1
-\cite_engine basic
-\cite_engine_type default
-\biblio_style plain
-\use_bibtopic false
-\use_indices false
-\paperorientation portrait
-\suppress_date false
-\justification true
-\use_refstyle 1
-\use_minted 0
-\index Index
-\shortcut idx
-\color #008000
-\end_index
-\leftmargin 0.2cm
-\topmargin 0.7cm
-\rightmargin 0.2cm
-\bottommargin 0.7cm
-\secnumdepth 3
-\tocdepth 3
-\paragraph_separation indent
-\paragraph_indentation default
-\is_math_indent 0
-\math_numbering_side default
-\quotes_style swiss
-\dynamic_quotes 0
-\papercolumns 1
-\papersides 1
-\paperpagestyle empty
-\tracking_changes false
-\output_changes false
-\html_math_output 0
-\html_css_as_file 0
-\html_be_strict false
-\end_header
-
-\begin_body
-
-\begin_layout Title
-Fundamentos Lógicos de la Informática
-\end_layout
-
-\begin_layout Date
-\begin_inset Note Note
-status open
-
-\begin_layout Plain Layout
-
-\end_layout
-
-\end_inset
-
-
-\end_layout
-
-\begin_layout Standard
-\begin_inset ERT
-status open
-
-\begin_layout Plain Layout
-
-
-\backslash
-def
-\backslash
-cryear{2017}
-\end_layout
-
-\end_inset
-
-
-\end_layout
-
-\begin_layout Standard
-\begin_inset CommandInset include
-LatexCommand input
-filename "../license.lyx"
-
-\end_inset
-
-
-\end_layout
-
-\begin_layout Standard
-Bibliografía:
-\end_layout
-
-\begin_layout Itemize
-Diapositivas de Fundamentos Lógicos de la Informática, Departamento de Ingenierí
-a de al Información y las Comunicaciones (nota: la errata es de ellos),
- Facultad de Informática, Universidad de Murcia.
-\end_layout
-
-\begin_layout Itemize
-Wikipedia, la enciclopedia libre (
-\begin_inset Flex URL
-status open
-
-\begin_layout Plain Layout
-
-https://es.wikipedia.org/
-\end_layout
-
-\end_inset
-
-).
-\end_layout
-
-\begin_layout Chapter
-Lógica
-\end_layout
-
-\begin_layout Standard
-\begin_inset CommandInset include
-LatexCommand input
-filename "n1.lyx"
-
-\end_inset
-
-
-\end_layout
-
-\begin_layout Chapter
-Lógica proposicional
-\end_layout
-
-\begin_layout Standard
-\begin_inset CommandInset include
-LatexCommand input
-filename "n2.lyx"
-
-\end_inset
-
-
-\end_layout
-
-\begin_layout Chapter
-Problema SAT
-\end_layout
-
-\begin_layout Standard
-\begin_inset CommandInset include
-LatexCommand input
-filename "n3.lyx"
-
-\end_inset
-
-
-\end_layout
-
-\begin_layout Chapter
-Deducción natural
-\end_layout
-
-\begin_layout Standard
-\begin_inset CommandInset include
-LatexCommand input
-filename "n4.lyx"
-
-\end_inset
-
-
-\end_layout
-
-\begin_layout Chapter
-Lógica categórica
-\end_layout
-
-\begin_layout Standard
-\begin_inset CommandInset include
-LatexCommand input
-filename "n5.lyx"
-
-\end_inset
-
-
-\end_layout
-
-\begin_layout Chapter
-Lógica de predicados de primer orden
-\end_layout
-
-\begin_layout Standard
-\begin_inset CommandInset include
-LatexCommand input
-filename "n6.lyx"
-
-\end_inset
-
-
-\end_layout
-
-\begin_layout Chapter
-Sistemas deductivos, razonamientos y deducciones
-\end_layout
-
-\begin_layout Standard
-\begin_inset CommandInset include
-LatexCommand input
-filename "n7.lyx"
-
-\end_inset
-
-
-\end_layout
-
-\end_body
-\end_document
diff --git a/logic/n1.lyx b/logic/n1.lyx
deleted file mode 100644
index 166b2b3..0000000
--- a/logic/n1.lyx
+++ /dev/null
@@ -1,346 +0,0 @@
-#LyX 2.3 created this file. For more info see http://www.lyx.org/
-\lyxformat 544
-\begin_document
-\begin_header
-\save_transient_properties true
-\origin unavailable
-\textclass book
-\use_default_options true
-\maintain_unincluded_children false
-\language spanish
-\language_package default
-\inputencoding auto
-\fontencoding global
-\font_roman "default" "default"
-\font_sans "default" "default"
-\font_typewriter "default" "default"
-\font_math "auto" "auto"
-\font_default_family default
-\use_non_tex_fonts false
-\font_sc false
-\font_osf false
-\font_sf_scale 100 100
-\font_tt_scale 100 100
-\use_microtype false
-\use_dash_ligatures true
-\graphics default
-\default_output_format default
-\output_sync 0
-\bibtex_command default
-\index_command default
-\paperfontsize default
-\spacing single
-\use_hyperref false
-\papersize default
-\use_geometry false
-\use_package amsmath 1
-\use_package amssymb 1
-\use_package cancel 1
-\use_package esint 1
-\use_package mathdots 1
-\use_package mathtools 1
-\use_package mhchem 1
-\use_package stackrel 1
-\use_package stmaryrd 1
-\use_package undertilde 1
-\cite_engine basic
-\cite_engine_type default
-\biblio_style plain
-\use_bibtopic false
-\use_indices false
-\paperorientation portrait
-\suppress_date false
-\justification true
-\use_refstyle 1
-\use_minted 0
-\index Index
-\shortcut idx
-\color #008000
-\end_index
-\secnumdepth 3
-\tocdepth 3
-\paragraph_separation indent
-\paragraph_indentation default
-\is_math_indent 0
-\math_numbering_side default
-\quotes_style swiss
-\dynamic_quotes 0
-\papercolumns 1
-\papersides 1
-\paperpagestyle default
-\tracking_changes false
-\output_changes false
-\html_math_output 0
-\html_css_as_file 0
-\html_be_strict false
-\end_header
-
-\begin_body
-
-\begin_layout Standard
-La lógica estudia las oraciones y los razonamientos, y existen tantas como
- tipos de oraciones y razonamientos.
- En informática, es la base de la programación, representa el conocimiento
- en inteligencia artificial, sirve para demostraciones de resultados teóricos
- y diseño de circuitos lógicos y define los problemas NP-completos (SAT).
- Existen distintas lógicas, como las lógicas clásicas (proposicional, categórica
-, de primer orden...) y la lógica difusa.
-\end_layout
-
-\begin_layout Section
-Oraciones
-\end_layout
-
-\begin_layout Standard
-Dentro de una misma lógica, una oración lógica es una oración del lenguaje
- natural que cumpla ciertas condiciones.
- En las lógicas clásicas, es aquella que es 
-\series bold
-enunciativa
-\series default
- y cumple la 
-\series bold
-ley del tercero excluido
-\series default
- (solo puede ser verdadera [
-\begin_inset Formula $V$
-\end_inset
-
-] o falsa [
-\begin_inset Formula $F$
-\end_inset
-
-]) y la 
-\series bold
-ley de no contradicción
-\series default
- (no puede ser 
-\begin_inset Formula $V$
-\end_inset
-
- y 
-\begin_inset Formula $F$
-\end_inset
-
- a la vez).
- Estas pueden ser 
-\series bold
-simples
-\series default
- (
-\series bold
-atómicas
-\series default
-) o 
-\series bold
-compuestas
-\series default
- (
-\series bold
-moleculares
-\series default
-), dependiendo de si tienen uno o más predicados.
-\end_layout
-
-\begin_layout Section
-Razonamientos
-\end_layout
-
-\begin_layout Standard
-Un razonamiento es una estructura que enlaza oraciones, de las cuales una
- es la 
-\series bold
-conclusión
-\series default
- de otras (
-\series bold
-premisas
-\series default
-) y todas (salvo ella misma) proporcionan evidencias para justificarla.
- Así, un razonamiento está formado por 
-\series bold
-axiomas
-\series default
- o 
-\series bold
-premisas
-\series default
-; 
-\series bold
-conclusiones
-\series default
- o 
-\series bold
-teoremas
-\series default
-, y una 
-\series bold
-demostración
-\series default
-.
- Existen dos tipos de razonamiento:
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Deductivo:
-\series default
- Se basa en la implicación.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Inductivo:
-\series default
- Parte de casos y llega a una conclusión general.
- Sólo es válido si se consideran todos los casos; de lo contrario la conclusión
- es probablemente, pero no necesariamente, cierta.
-\end_layout
-
-\begin_layout Standard
-Un razonamiento es válido si la conclusión es necesariamente cierta cuando
- lo son las premisas, y se escribe como 
-\begin_inset Formula $\underset{\text{Premisas}}{\{\alpha_{1},\alpha_{2},\dots,\alpha_{n}\}}\vDash\underset{\text{Conclusión}}{\beta}$
-\end_inset
-
-.
- Para representarlo:
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Representación gráfica:
-\series default
-
-\begin_inset Formula 
-\[
-\begin{array}{ccccc}
-P_{1} & \land & P_{2}\\
-\hline  & \downarrow\\
- & C_{1} &  & \land & P_{3}\\
-\hline  &  &  & \downarrow\\
- &  &  & C_{2}
-\end{array}
-\]
-
-\end_inset
-
-
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Representación estándar:
-\begin_inset Formula 
-\[
-\begin{array}{ccc}
- & P_{1}\\
- & P_{2}\\
-\hline \therefore & C_{1} & P_{1}\text{ y }P_{2}\\
- & P_{3}\\
-\hline \therefore & C_{2} & C_{1}\text{ y }P_{3}
-\end{array}
-\]
-
-\end_inset
-
-
-\end_layout
-
-\begin_layout Section
-Tipos de definiciones
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Extensiva
-\series default
- o 
-\series bold
-extensional:
-\series default
- Lista de elementos que cumplen la condición.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Comprensiva
-\series default
- o 
-\series bold
-intensional:
-\series default
- Lista de propiedades necesarias.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Recursiva:
-\series default
- Formada por una 
-\series bold
-regla base
-\series default
-, que define casos concretos, y una 
-\series bold
-regla recursiva
-\series default
-, que define todos los demás casos a partir de casos ya conocidos mediante
- una relación.
- También puede contener una 
-\series bold
-regla de exclusión
-\series default
-.
-\end_layout
-
-\begin_layout Section
-Lenguajes formales
-\end_layout
-
-\begin_layout Standard
-El lenguaje natural es ambiguo, y suele ser vago, paradójico, complicado...
- Por tanto, en ciencia es imprescindible un lenguaje formal para obtener
- rigor.
- Un lenguaje formal consta de un conjunto de símbolos (
-\series bold
-alfabeto
-\series default
- o 
-\series bold
-vocabulario
-\series default
-) y una definición recursiva para conectarlos (
-\series bold
-gramática
-\series default
- o 
-\series bold
-sintaxis
-\series default
-), y es el conjunto de todas las fórmulas bien formadas (f.b.f.) obtenidas
- a partir de estas.
- En la práctica, necesitamos un sistema de codificación (formalización)
- y de interpretación.
-\end_layout
-
-\begin_layout Section
-Formalización e interpretación
-\end_layout
-
-\begin_layout Standard
-Formalizar es obtener una oración o f.b.f.
- en lenguaje formal a partir del lenguaje natural, mientras que interpretar
- es entender una f.b.f.
- expresándola en lenguaje natural.
-\end_layout
-
-\end_body
-\end_document
diff --git a/logic/n2.lyx b/logic/n2.lyx
deleted file mode 100644
index 93478b7..0000000
--- a/logic/n2.lyx
+++ /dev/null
@@ -1,1518 +0,0 @@
-#LyX 2.3 created this file. For more info see http://www.lyx.org/
-\lyxformat 544
-\begin_document
-\begin_header
-\save_transient_properties true
-\origin unavailable
-\textclass book
-\use_default_options true
-\maintain_unincluded_children false
-\language spanish
-\language_package default
-\inputencoding auto
-\fontencoding global
-\font_roman "default" "default"
-\font_sans "default" "default"
-\font_typewriter "default" "default"
-\font_math "auto" "auto"
-\font_default_family default
-\use_non_tex_fonts false
-\font_sc false
-\font_osf false
-\font_sf_scale 100 100
-\font_tt_scale 100 100
-\use_microtype false
-\use_dash_ligatures true
-\graphics default
-\default_output_format default
-\output_sync 0
-\bibtex_command default
-\index_command default
-\paperfontsize default
-\spacing single
-\use_hyperref false
-\papersize default
-\use_geometry false
-\use_package amsmath 1
-\use_package amssymb 1
-\use_package cancel 1
-\use_package esint 1
-\use_package mathdots 1
-\use_package mathtools 1
-\use_package mhchem 1
-\use_package stackrel 1
-\use_package stmaryrd 1
-\use_package undertilde 1
-\cite_engine basic
-\cite_engine_type default
-\biblio_style plain
-\use_bibtopic false
-\use_indices false
-\paperorientation portrait
-\suppress_date false
-\justification true
-\use_refstyle 1
-\use_minted 0
-\index Index
-\shortcut idx
-\color #008000
-\end_index
-\secnumdepth 3
-\tocdepth 3
-\paragraph_separation indent
-\paragraph_indentation default
-\is_math_indent 0
-\math_numbering_side default
-\quotes_style swiss
-\dynamic_quotes 0
-\papercolumns 1
-\papersides 1
-\paperpagestyle default
-\tracking_changes false
-\output_changes false
-\html_math_output 0
-\html_css_as_file 0
-\html_be_strict false
-\end_header
-
-\begin_body
-
-\begin_layout Standard
-Las oraciones lógicas en lógica proposicional (
-\series bold
-L0
-\series default
-) se llaman 
-\series bold
-proposiciones
-\series default
-.
- Las proposiciones atómicas, también llamadas 
-\series bold
-sentencias
-\series default
- o 
-\series bold
-átomos
-\series default
-, se agrupan mediante 
-\series bold
-operadores lógicos
-\series default
- para formar oraciones compuestas.
-\end_layout
-
-\begin_layout Section
-Sintaxis
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Constantes:
-\series default
- Verdadero (
-\begin_inset Formula $V$
-\end_inset
-
-) o falso (
-\begin_inset Formula $F$
-\end_inset
-
-).
- 
-\begin_inset Formula $\mathbb{B}=\{V,F\}$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Sentencias:
-\series default
- Se representan por un conjunto de letras latinas.
- El conjunto de todos se denota por 
-\begin_inset Formula ${\cal P}$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Operadores lógicos:
-\series default
- Negación (
-\begin_inset Formula $\neg$
-\end_inset
-
-) y conectivos.
- Los conectivos son: conjunción (
-\begin_inset Formula $\land$
-\end_inset
-
-), disyunción (
-\begin_inset Formula $\lor$
-\end_inset
-
-), implicación (
-\begin_inset Formula $\rightarrow$
-\end_inset
-
-) y doble implicación (
-\begin_inset Formula $\leftrightarrow$
-\end_inset
-
-).
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Paréntesis
-\series default
- o corchetes, para agrupar expresiones.
-\end_layout
-
-\begin_layout Standard
-Definición recursiva de una f.b.f.:
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Forma básica:
-\series default
- Todo átomo es una f.b.f.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Forma recursiva:
-\series default
- Si 
-\begin_inset Formula $\alpha$
-\end_inset
-
- y 
-\begin_inset Formula $\beta$
-\end_inset
-
- son f.b.f., también lo son 
-\begin_inset Formula $\neg\alpha$
-\end_inset
-
-, 
-\begin_inset Formula $(\alpha\land\beta)$
-\end_inset
-
-, 
-\begin_inset Formula $(\alpha\lor\beta)$
-\end_inset
-
-, 
-\begin_inset Formula $(\alpha\rightarrow\beta)$
-\end_inset
-
- y 
-\begin_inset Formula $(\alpha\leftrightarrow\beta)$
-\end_inset
-
-.
- La presencia o ausencia de paréntesis es importante.
-\end_layout
-
-\begin_layout Standard
-En la práctica, podemos eliminar paréntesis según estas reglas:
-\end_layout
-
-\begin_layout Itemize
-Se pueden eliminar los paréntesis exteriores.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Prioridad:
-\series default
- De mayor a menor: 
-\begin_inset Formula $\neg$
-\end_inset
-
-, (
-\begin_inset Formula $\land$
-\end_inset
-
-, 
-\begin_inset Formula $\lor$
-\end_inset
-
-), (
-\begin_inset Formula $\rightarrow$
-\end_inset
-
-, 
-\begin_inset Formula $\leftrightarrow$
-\end_inset
-
-).
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Asociatividad:
-\series default
- A igual prioridad de operadores, se asocia por la izquierda.
-\end_layout
-
-\begin_layout Standard
-También podemos añadir paréntesis a cualquier expresión que no sea una negación.
-\end_layout
-
-\begin_layout Section
-Formalización
-\end_layout
-
-\begin_layout Itemize
-Los átomos corresponden a oraciones enunciativas afirmativas, en forma presente
- y con sujeto (salvo verbos impersonales).
-\end_layout
-
-\begin_layout Itemize
-\begin_inset Formula $\neg\alpha$
-\end_inset
-
-: No 
-\begin_inset Formula $\alpha$
-\end_inset
-
-, no es el caso de 
-\begin_inset Formula $\alpha$
-\end_inset
-
-, no es cierto que 
-\begin_inset Formula $\alpha$
-\end_inset
-
-, es falso que 
-\begin_inset Formula $\alpha$
-\end_inset
-
-, no sucede que 
-\begin_inset Formula $\alpha$
-\end_inset
-
-, la negación de 
-\begin_inset Formula $\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-\begin_inset Formula $\alpha\land\beta$
-\end_inset
-
-: 
-\begin_inset Formula $\alpha$
-\end_inset
-
- y 
-\begin_inset Formula $\beta$
-\end_inset
-
- (pero, aunque, además, sin embargo, también, a la vez, aún, no obstante).
-\end_layout
-
-\begin_layout Itemize
-\begin_inset Formula $\alpha\lor\beta$
-\end_inset
-
-: O 
-\begin_inset Formula $\alpha$
-\end_inset
-
- o 
-\begin_inset Formula $\beta$
-\end_inset
-
-; ya 
-\begin_inset Formula $\alpha$
-\end_inset
-
-, ya 
-\begin_inset Formula $\beta$
-\end_inset
-
-, ya ambas.
-\end_layout
-
-\begin_layout Itemize
-\begin_inset Formula $\alpha\rightarrow\beta$
-\end_inset
-
-: Si 
-\begin_inset Formula $\alpha$
-\end_inset
-
- 
-\begin_inset Formula $\beta$
-\end_inset
-
-, si 
-\begin_inset Formula $\alpha$
-\end_inset
-
- entonces 
-\begin_inset Formula $\beta$
-\end_inset
-
-, 
-\begin_inset Formula $\alpha$
-\end_inset
-
- solo si 
-\begin_inset Formula $\beta$
-\end_inset
-
-, solo 
-\begin_inset Formula $\alpha$
-\end_inset
-
- si 
-\begin_inset Formula $\beta$
-\end_inset
-
-, es suficiente 
-\begin_inset Formula $\alpha$
-\end_inset
-
- para que 
-\begin_inset Formula $\beta$
-\end_inset
-
-, siempre que 
-\begin_inset Formula $\alpha$
-\end_inset
-
- entonces 
-\begin_inset Formula $\beta$
-\end_inset
-
-, no 
-\begin_inset Formula $\alpha$
-\end_inset
-
- a menos que 
-\begin_inset Formula $\beta$
-\end_inset
-
-, es necesario 
-\begin_inset Formula $\beta$
-\end_inset
-
- para que 
-\begin_inset Formula $\alpha$
-\end_inset
-
-, a no ser que 
-\begin_inset Formula $\beta$
-\end_inset
-
- no 
-\begin_inset Formula $\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-\begin_inset Formula $\alpha\leftrightarrow\beta$
-\end_inset
-
-: 
-\begin_inset Formula $\alpha$
-\end_inset
-
- si y sólo si 
-\begin_inset Formula $\beta$
-\end_inset
-
-, 
-\begin_inset Formula $\alpha$
-\end_inset
-
- equivale a 
-\begin_inset Formula $\beta$
-\end_inset
-
-, 
-\begin_inset Formula $\alpha$
-\end_inset
-
- cuando y sólo cuando 
-\begin_inset Formula $\beta$
-\end_inset
-
-, 
-\begin_inset Formula $\alpha$
-\end_inset
-
- cuando únicamente 
-\begin_inset Formula $\beta$
-\end_inset
-
- , 
-\begin_inset Formula $\alpha$
-\end_inset
-
- es condición suficiente y necesaria para que 
-\begin_inset Formula $\beta$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Section
-Interpretación
-\end_layout
-
-\begin_layout Standard
-Procedimiento que traduce las fórmulas 
-\series bold
-atómicas
-\series default
- a oraciones naturales.
- Una 
-\series bold
-asignación
-\series default
- 
-\begin_inset Formula $v_{I}$
-\end_inset
-
- es el procedimiento que establece un valor de verdad a una fórmula atómica
- según una interpretación 
-\begin_inset Formula $I$
-\end_inset
-
-.
- En L0 no se suele hacer distinción, y hace referencia a una función 
-\begin_inset Formula $v_{I}:{\cal P_{\alpha}}\rightarrow\mathbb{B}$
-\end_inset
-
- tal que 
-\begin_inset Formula $V\mapsto V$
-\end_inset
-
- y 
-\begin_inset Formula $F\mapsto F$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Standard
-La 
-\series bold
-evaluación
-\series default
- es la obtención del valor de verdad de una oración 
-\begin_inset Formula $\alpha$
-\end_inset
-
-.
- Decimos 
-\begin_inset Formula $V(\alpha)=V$
-\end_inset
-
- o 
-\begin_inset Formula $V(\alpha)=F$
-\end_inset
-
-, según corresponda.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Regla base:
-\series default
- Si 
-\begin_inset Formula $\alpha\in{\cal P}$
-\end_inset
-
-, entonces 
-\begin_inset Formula $V(\alpha)=v_{I}(\alpha)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Regla recursiva:
-\series default
-
-\begin_inset Formula 
-\begin{eqnarray*}
-V(\neg\alpha) & = & \begin{cases}
-V & \text{si }V(\alpha)=F\\
-F & \text{si }V(\alpha)=V
-\end{cases}\\
-V(\alpha\land\beta) & = & \begin{cases}
-V & \text{si }V(\alpha)=V\text{ y }V(\beta)=V\\
-F & \text{en otro caso}
-\end{cases}\\
-V(\alpha\lor\beta) & = & \begin{cases}
-F & \text{si }V(\alpha)=F\text{ y }V(\beta)=F\\
-V & \text{en otro caso}
-\end{cases}\\
-V(\alpha\rightarrow\beta) & = & \begin{cases}
-F & \text{si }V(\alpha)=V\text{ y }V(\beta)=F\\
-V & \text{en otro caso}
-\end{cases}\\
-V(\alpha\leftrightarrow\beta) & = & \begin{cases}
-V & \text{si }V(\alpha)=V(\beta)\\
-F & \text{en otro caso}
-\end{cases}
-\end{eqnarray*}
-
-\end_inset
-
-
-\end_layout
-
-\begin_layout Section
-Grafos semánticos
-\end_layout
-
-\begin_layout Standard
-Un grafo semántico es un árbol que representa una f.b.f.
- El nodo principal contiene el operador principal (o el único átomo).
- De cada conectivo parten dos ramas (o una si es 
-\begin_inset Formula $\neg$
-\end_inset
-
-) con las subfórmulas que conecta, y los átomos son hojas.
-\end_layout
-
-\begin_layout Section
-Decidibilidad
-\end_layout
-
-\begin_layout Standard
-Una oración puede ser:
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Satisfacible
-\series default
- si 
-\begin_inset Formula $V(\alpha)=V$
-\end_inset
-
- en alguna interpretación.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Falseable
-\series default
- si 
-\begin_inset Formula $V(\alpha)=F$
-\end_inset
-
- en alguna interpretación.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Contingente
-\series default
- o 
-\series bold
-contingencia
-\series default
- si es a la vez satisfacible y falseable.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Tautológica
-\series default
-, 
-\series bold
-válida
-\series default
- o 
-\series bold
-tautología
-\series default
- si 
-\begin_inset Formula $V(\alpha)=V$
-\end_inset
-
- en todas las interpretaciones.
- Escribimos 
-\begin_inset Formula $\vDash\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Insatisfacible
-\series default
- o 
-\series bold
-contradicción
-\series default
- si 
-\begin_inset Formula $V(\alpha)=F$
-\end_inset
-
- en todas las interpretaciones.
-\end_layout
-
-\begin_layout Standard
-El problema SAT, determinar si una oración lógica es satisfacible, es el
- primer problema conocido NP-completo, y de hecho todos los problemas NP-complet
-os se pueden reducir a SAT, de modo que si uno de resuelve como P, se resuelven
- todos.
-\end_layout
-
-\begin_layout Standard
-Un conjunto de fórmulas 
-\begin_inset Formula ${\cal F}=\{\alpha_{1},\dots,\alpha_{n}\}$
-\end_inset
-
- es satisfacible si su conjunción lo es, y llamamos 
-\series bold
-modelo
-\series default
- de 
-\begin_inset Formula ${\cal F}$
-\end_inset
-
- a cualquier interpretación en la que 
-\begin_inset Formula $V(\alpha_{1}\land\dots\land\alpha_{n})=V$
-\end_inset
-
-.
- Definimos del mismo modo conjunto insatisfacible.
- El conjunto 
-\begin_inset Formula ${\cal F}=\{\}$
-\end_inset
-
- es modelo en todas las interpretaciones.
-\end_layout
-
-\begin_layout Standard
-Para hallar los valores de verdad de una oración en función de la interpretación
-, podemos construir una 
-\series bold
-tabla de verdad.
-
-\series default
- Si 
-\begin_inset Formula $\alpha$
-\end_inset
-
- tiene 
-\begin_inset Formula $n$
-\end_inset
-
- átomos y 
-\begin_inset Formula $m$
-\end_inset
-
- operadores, construimos una tabla con 
-\begin_inset Formula $2^{n}$
-\end_inset
-
- filas (más la cabecera) y 
-\begin_inset Formula $n+m$
-\end_inset
-
- columnas.
- En cada fila establecemos una asignación hasta establecer todas las asignacione
-s posibles y obtenemos las evaluaciones para las oraciones definidas por
- cada operador, en orden de evaluación y terminando con el operador principal,
- que establece el valor de verdad.
- Debemos indicar el orden de evaluación.
-\end_layout
-
-\begin_layout Standard
-Otra forma es la 
-\series bold
-propagación de literales.
-
-\series default
- Un literal es un átomo o la negación de un átomo.
- Dada una fórmula 
-\begin_inset Formula $\phi$
-\end_inset
-
-, definimos 
-\begin_inset Formula $\phi(p)\equiv\phi_{|V(p)=V}$
-\end_inset
-
- a la fórmula más simplificada que, en las interpretaciones en las que 
-\begin_inset Formula $V(p)=V$
-\end_inset
-
-, tenga los mismos valores de verdad que 
-\begin_inset Formula $\phi$
-\end_inset
-
-.
- Por ejemplo, dada la oración 
-\begin_inset Formula $\phi\equiv(p\rightarrow q)\rightarrow(\neg p\rightarrow\neg q)$
-\end_inset
-
-, tendríamos que 
-\begin_inset Formula $\phi(p)\equiv\phi_{|V(p)=V}\equiv(V\rightarrow q)\rightarrow(\neg V\rightarrow\neg q)\equiv q\rightarrow(F\rightarrow q)\equiv q\rightarrow V\equiv V$
-\end_inset
-
-, mientras que 
-\begin_inset Formula $\phi(\neg p)\equiv\phi_{|V(\neg p)=V}\equiv\phi_{|V(p)=F}\equiv(F\rightarrow q)\rightarrow(\neg F\rightarrow\neg q)\equiv V\rightarrow(V\rightarrow\neg q)\equiv V\rightarrow\neg q\equiv\neg q$
-\end_inset
-
-.
- En el segundo caso, tendríamos, por ejemplo, que 
-\begin_inset Formula $\phi(\neg p)(q)\equiv\phi(\neg p,q)\equiv\phi(\neg p)_{|V(q)=V}\equiv\neg V\equiv F$
-\end_inset
-
-.
- En la práctica bastaría con escribir 
-\begin_inset Formula $\phi(\neg p,q)\equiv\neg V\equiv F$
-\end_inset
-
- para este último caso.
-\end_layout
-
-\begin_layout Standard
-Para comprobar los valores de verdad realizaríamos un 
-\series bold
-árbol semántico.
-
-\series default
- En este, la raíz sería la fórmula inicial, y de cada nodo, que contendrá
- una fórmula 
-\begin_inset Formula $\xi$
-\end_inset
-
-, partirán dos ramas con 
-\begin_inset Formula $\xi(p)$
-\end_inset
-
- y 
-\begin_inset Formula $\xi(\neg p)$
-\end_inset
-
- para algún átomo 
-\begin_inset Formula $l$
-\end_inset
-
- en 
-\begin_inset Formula $\xi$
-\end_inset
-
- (normalmente el que más aparece), salvo si 
-\begin_inset Formula $\xi\equiv V$
-\end_inset
-
- o 
-\begin_inset Formula $\xi\equiv F$
-\end_inset
-
-.
- A la hora de dibujarlo, la línea que une una expresión con otra derivada
- se etiqueta con el literal a propagar.
-\end_layout
-
-\begin_layout Section
-Equivalencias
-\end_layout
-
-\begin_layout Standard
-Dos expresiones 
-\begin_inset Formula $\alpha$
-\end_inset
-
- y 
-\begin_inset Formula $\beta$
-\end_inset
-
- son lógicamente equivalentes si y sólo si 
-\begin_inset Formula $V(\alpha)=V(\beta)$
-\end_inset
-
- para cualquier interpretación.
- Escribimos 
-\begin_inset Formula $\alpha\equiv\beta$
-\end_inset
-
-.
- Así, 
-\begin_inset Formula $\alpha\equiv\beta\iff\vDash\alpha\leftrightarrow\beta$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Propiedades conmutativas:
-\series default
- 
-\begin_inset Formula $\alpha\land\beta\equiv\beta\land\alpha$
-\end_inset
-
-; 
-\begin_inset Formula $\alpha\lor\beta\equiv\beta\land\alpha$
-\end_inset
-
-; 
-\begin_inset Formula $\alpha\leftrightarrow\beta\equiv\beta\leftrightarrow\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Propiedades asociativas:
-\series default
- 
-\begin_inset Formula $\alpha\land(\beta\land\gamma)\equiv(\alpha\land\beta)\land\gamma$
-\end_inset
-
-; 
-\begin_inset Formula $\alpha\lor(\beta\lor\gamma)\equiv(\alpha\lor\beta)\lor\gamma$
-\end_inset
-
-; 
-\begin_inset Formula $\alpha\leftrightarrow(\beta\leftrightarrow\gamma)\equiv(\alpha\leftrightarrow\beta)\leftrightarrow\gamma$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Propiedades de De Morgan:
-\series default
- 
-\begin_inset Formula $\neg(\alpha\land\beta)\equiv\neg\alpha\lor\neg\beta$
-\end_inset
-
-; 
-\begin_inset Formula $\neg(\alpha\lor\beta)\equiv\neg\alpha\land\neg\beta$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Propiedades distributivas:
-\series default
- 
-\begin_inset Formula $\alpha\land(\beta\lor\gamma)\equiv(\alpha\land\beta)\lor(\alpha\land\gamma)$
-\end_inset
-
-; 
-\begin_inset Formula $\alpha\lor(\beta\land\gamma)\equiv(\alpha\lor\beta)\land(\alpha\lor\gamma)$
-\end_inset
-
-; 
-\begin_inset Formula $\alpha\rightarrow(\beta\lor\gamma)\equiv(\alpha\rightarrow\beta)\lor(\alpha\rightarrow\gamma)$
-\end_inset
-
-; 
-\begin_inset Formula $\alpha\rightarrow(\beta\land\gamma)\equiv(\alpha\rightarrow\beta)\land(\alpha\rightarrow\gamma)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Propiedades de absorción:
-\series default
- 
-\begin_inset Formula $\alpha\lor(\alpha\land\beta)\equiv\alpha\land(\alpha\lor\beta)\equiv\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Expresión booleana:
-\series default
- 
-\begin_inset Formula $\alpha\lor(\neg\beta\land\beta)\equiv\alpha\land(\neg\beta\lor\beta)\equiv\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Reducción al absurdo:
-\series default
- 
-\begin_inset Formula $\neg\alpha\rightarrow(\beta\land\neg\beta)\equiv\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Propiedad de contraposición
-\series default
- o 
-\series bold
-transposición:
-\series default
- 
-\begin_inset Formula $\alpha\rightarrow\beta\equiv\neg\beta\rightarrow\neg\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Exportación:
-\series default
- 
-\begin_inset Formula $(\alpha\land\beta)\rightarrow\gamma\equiv\alpha\rightarrow(\beta\rightarrow\gamma)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Idempotencia:
-\series default
- 
-\begin_inset Formula $\alpha\equiv\neg(\neg\alpha)\equiv\alpha\lor\alpha\equiv\alpha\land\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Eliminación del condicional:
-\series default
- 
-\begin_inset Formula $\alpha\rightarrow\beta\equiv\neg\alpha\lor\beta\equiv\neg(\alpha\land\neg\beta)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Eliminación del bicondicional:
-\series default
- 
-\begin_inset Formula $\alpha\leftrightarrow\beta\equiv(\alpha\rightarrow\beta)\land(\beta\rightarrow\alpha)\equiv(\alpha\land\beta)\lor(\neg\beta\land\neg\alpha)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Propiedades sobre tautologías:
-\series default
- 
-\begin_inset Formula $\alpha\lor\neg\alpha\equiv V$
-\end_inset
-
-; 
-\begin_inset Formula $V\lor\beta\equiv V$
-\end_inset
-
-; 
-\begin_inset Formula $V\land\beta\equiv\beta$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Propiedades sobre insatisfacibilidad:
-\series default
- 
-\begin_inset Formula $\alpha\land\neg\alpha\equiv F$
-\end_inset
-
-; 
-\begin_inset Formula $F\lor\beta\equiv\beta$
-\end_inset
-
-; 
-\begin_inset Formula $F\land\beta\equiv F$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Section
-Razonamientos válidos
-\end_layout
-
-\begin_layout Standard
-Un razonamiento es válido si y sólo si en todas las interpretaciones en
- las que 
-\begin_inset Formula $\alpha$
-\end_inset
-
- es verdad, 
-\begin_inset Formula $\beta$
-\end_inset
-
- también lo es.
- Igualmente, 
-\begin_inset Formula $\beta$
-\end_inset
-
- es 
-\series bold
-consecuencia lógica
-\series default
- de 
-\begin_inset Formula ${\cal F}=\{\alpha_{1},\dots,\alpha_{n}\}$
-\end_inset
-
- si 
-\begin_inset Formula $\beta$
-\end_inset
-
- es verdad siempre que 
-\begin_inset Formula ${\cal F}$
-\end_inset
-
- sea un modelo.
- Escribimos 
-\begin_inset Formula $\alpha\vDash\beta$
-\end_inset
-
- o 
-\begin_inset Formula ${\cal F}\vDash\beta$
-\end_inset
-
-, y sabemos que 
-\begin_inset Formula $\alpha\vDash\beta\iff\vDash\alpha\rightarrow\beta$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Standard
-
-\series bold
-Teorema de la deducción semántica:
-\series default
- 
-\begin_inset Formula ${\cal F}\cup\{\alpha\}\vDash\beta\iff{\cal F}\vDash\alpha\rightarrow\beta$
-\end_inset
-
-.
- Corolario: 
-\begin_inset Formula ${\cal F}\vDash\beta\iff\vDash\alpha_{1}\land\dots\land\alpha_{n}\rightarrow\beta\iff\vDash\neg(\alpha_{1}\land\dots\land\alpha_{n}\land\neg\beta)\iff\alpha_{1}\land\dots\land\alpha_{n}\land\neg\beta\text{ es insatisfacible}$
-\end_inset
-
-.
- Propiedades generales de 
-\begin_inset Formula $\vDash$
-\end_inset
-
-:
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Reflexividad:
-\series default
- 
-\begin_inset Formula $\alpha\vDash\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Transitividad:
-\series default
- Si 
-\begin_inset Formula ${\cal F}\vDash\alpha$
-\end_inset
-
- y 
-\begin_inset Formula $\alpha\vDash\beta$
-\end_inset
-
- entonces 
-\begin_inset Formula ${\cal F}\vDash\beta$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Monotonía:
-\series default
- Si 
-\begin_inset Formula ${\cal F}\vDash\alpha$
-\end_inset
-
- entonces 
-\begin_inset Formula ${\cal F}\cup\{\beta\}\vDash\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-Si 
-\begin_inset Formula ${\cal F}\vDash\alpha$
-\end_inset
-
- y 
-\begin_inset Formula $\vDash\beta$
-\end_inset
-
-, entonces 
-\begin_inset Formula ${\cal F}\backslash\{\beta\}\vDash\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-\begin_inset Formula $\alpha\equiv\beta\iff\alpha\vDash\beta\text{ y }\beta\vDash\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Standard
-Algunas propiedades:
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Simplificación
-\series default
- o 
-\series bold
-eliminación de la conjunción:
-\series default
- 
-\begin_inset Formula $\alpha\land\beta\vDash\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Adición
-\series default
- o 
-\series bold
-introducción de la disyunción:
-\series default
- 
-\begin_inset Formula $\alpha\vDash\alpha\lor\beta$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Silogismos:
-\series default
- Forma de razonamiento deductivo con dos premisas y una conclusión.
-\end_layout
-
-\begin_deeper
-\begin_layout Itemize
-
-\series bold
-Categóricos
-\end_layout
-
-\begin_deeper
-\begin_layout Itemize
-
-\series bold
-Combinación
-\series default
- o 
-\series bold
-introducción de la conjunción:
-\series default
- 
-\begin_inset Formula $\{\alpha,\beta\}\vDash\alpha\land\beta$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Inconsistencia:
-\series default
- 
-\begin_inset Formula $\{\alpha,\neg\alpha\}\vDash\beta$
-\end_inset
-
-.
-\end_layout
-
-\end_deeper
-\begin_layout Itemize
-
-\series bold
-Hipotéticos
-\end_layout
-
-\begin_deeper
-\begin_layout Itemize
-
-\series bold
-Silogismo hipotético:
-\series default
- 
-\begin_inset Formula $\{\alpha\rightarrow\beta,\beta\rightarrow\gamma\}\vDash\alpha\rightarrow\gamma$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Demostración por casos:
-\series default
- 
-\begin_inset Formula $\{\alpha\rightarrow\gamma,\beta\rightarrow\gamma\}\vDash\alpha\lor\beta\rightarrow\gamma$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Prueba por casos:
-\series default
- 
-\begin_inset Formula $\{\alpha\rightarrow\beta,\neg\alpha\rightarrow\beta\}\vDash\beta$
-\end_inset
-
-.
-\end_layout
-
-\end_deeper
-\begin_layout Itemize
-
-\series bold
-Hipotéticos mixtos
-\end_layout
-
-\begin_deeper
-\begin_layout Itemize
-
-\series bold
-Modus Ponens:
-\series default
- 
-\begin_inset Formula $\{\alpha\rightarrow\beta,\alpha\}\vDash\beta$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Modus Tollens:
-\series default
- 
-\begin_inset Formula $\{\alpha\rightarrow\beta,\neg\beta\}\vDash\neg\alpha$
-\end_inset
-
-.
-\end_layout
-
-\end_deeper
-\begin_layout Itemize
-
-\series bold
-Disyuntivo:
-\series default
- 
-\begin_inset Formula $\{\alpha\lor\beta,\neg\beta\}\vDash\alpha$
-\end_inset
-
-.
-\end_layout
-
-\end_deeper
-\begin_layout Itemize
-
-\series bold
-Dilemas:
-\series default
- Forma de razonamiento con una premisa disyunción que representa las opciones,
- normalmente contrarias.
-\end_layout
-
-\begin_deeper
-\begin_layout Itemize
-
-\series bold
-Constructivo:
-\series default
- 
-\begin_inset Formula $\{\alpha\lor\beta,\alpha\rightarrow\gamma,\beta\rightarrow\delta\}\vDash\gamma\lor\delta$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Destructivo:
-\series default
- 
-\begin_inset Formula $\{\neg\gamma\lor\neg\delta,\alpha\rightarrow\gamma,\beta\rightarrow\delta\}\vDash\neg\alpha\lor\neg\beta$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Transposición:
-\series default
- 
-\begin_inset Formula $\alpha\rightarrow\beta\vDash\neg\beta\rightarrow\neg\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Eliminación de la equivalencia:
-\series default
- 
-\begin_inset Formula $\alpha\leftrightarrow\beta\vDash\{\alpha\rightarrow\beta,\beta\rightarrow\alpha\}$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Introducción de la equivalencia:
-\series default
- 
-\begin_inset Formula $\{\alpha\rightarrow\beta,\beta\rightarrow\alpha\}\vDash\alpha\leftrightarrow\beta$
-\end_inset
-
-.
-\end_layout
-
-\end_deeper
-\begin_layout Standard
-El Corolario del Teorema de la Deducción Semántica y las propiedades básicas
- de equivalencia y razonamientos nos permiten considerar al menos dos estrategia
-s de razonamiento deductivo: la 
-\series bold
-demostración directa
-\series default
-, comprobando que 
-\begin_inset Formula $\beta$
-\end_inset
-
- es consecuencia lógica de 
-\begin_inset Formula $\alpha$
-\end_inset
-
- mediante definiciones, tautologías, teoremas o propiedades, y 
-\series bold
-refutación
-\series default
- o demostración por contradicción (
-\begin_inset Formula $\alpha\rightarrow\beta\equiv\alpha\land\neg\beta\implies\gamma\land\neg\gamma$
-\end_inset
-
-), buscando contraejemplos o encontrando un 
-\begin_inset Formula $a$
-\end_inset
-
- tal que 
-\begin_inset Formula $V(\alpha[a]\rightarrow\beta[a])=F$
-\end_inset
-
-.
-\end_layout
-
-\end_body
-\end_document
diff --git a/logic/n3.lyx b/logic/n3.lyx
deleted file mode 100644
index f720c27..0000000
--- a/logic/n3.lyx
+++ /dev/null
@@ -1,1512 +0,0 @@
-#LyX 2.3 created this file. For more info see http://www.lyx.org/
-\lyxformat 544
-\begin_document
-\begin_header
-\save_transient_properties true
-\origin unavailable
-\textclass book
-\use_default_options true
-\maintain_unincluded_children false
-\language spanish
-\language_package default
-\inputencoding auto
-\fontencoding global
-\font_roman "default" "default"
-\font_sans "default" "default"
-\font_typewriter "default" "default"
-\font_math "auto" "auto"
-\font_default_family default
-\use_non_tex_fonts false
-\font_sc false
-\font_osf false
-\font_sf_scale 100 100
-\font_tt_scale 100 100
-\use_microtype false
-\use_dash_ligatures true
-\graphics default
-\default_output_format default
-\output_sync 0
-\bibtex_command default
-\index_command default
-\paperfontsize default
-\spacing single
-\use_hyperref false
-\papersize default
-\use_geometry false
-\use_package amsmath 1
-\use_package amssymb 1
-\use_package cancel 1
-\use_package esint 1
-\use_package mathdots 1
-\use_package mathtools 1
-\use_package mhchem 1
-\use_package stackrel 1
-\use_package stmaryrd 1
-\use_package undertilde 1
-\cite_engine basic
-\cite_engine_type default
-\biblio_style plain
-\use_bibtopic false
-\use_indices false
-\paperorientation portrait
-\suppress_date false
-\justification true
-\use_refstyle 1
-\use_minted 0
-\index Index
-\shortcut idx
-\color #008000
-\end_index
-\secnumdepth 3
-\tocdepth 3
-\paragraph_separation indent
-\paragraph_indentation default
-\is_math_indent 0
-\math_numbering_side default
-\quotes_style swiss
-\dynamic_quotes 0
-\papercolumns 1
-\papersides 1
-\paperpagestyle default
-\tracking_changes false
-\output_changes false
-\html_math_output 0
-\html_css_as_file 0
-\html_be_strict false
-\end_header
-
-\begin_body
-
-\begin_layout Section
-Algoritmos que no requieren cláusulas
-\end_layout
-
-\begin_layout Subsection
-Tablas de verdad
-\end_layout
-
-\begin_layout Standard
-Construimos una tabla de verdad por filas, y si en una fila obtenemos que
- la oración es cierta para dicha interpretación, la oración es satisfacible.
- Si no es cierta en ninguna, la oración es insatisfacible.
-\end_layout
-
-\begin_layout Subsection
-Árboles semánticos
-\end_layout
-
-\begin_layout Standard
-Una hoja de un árbol semántico es un 
-\series bold
-nodo fallo
-\series default
- si su etiqueta es 
-\begin_inset Formula $F$
-\end_inset
-
-, y 
-\series bold
-nodo éxito
-\series default
- si es 
-\begin_inset Formula $V$
-\end_inset
-
-.
- Representamos el árbol como 
-\begin_inset Formula $\vernal$
-\end_inset
-
-, y observamos que, para comprobar la satisfacibilidad, basta con encontrar
- un nodo éxito, y entonces no es necesario seguir desarrollando.
-\end_layout
-
-\begin_layout Subsection
-Tableaux semánticos
-\end_layout
-
-\begin_layout Standard
-Un 
-\series bold
-tableaux semántico
-\series default
- es un árbol en el cual cada nodo está formado por una lista de oraciones
- (sin paréntesis de ningún tipo), y su raíz es la lista formada por la oración
- 
-\begin_inset Formula $\phi$
-\end_inset
-
- a desarrollar.
- Una oración puede tener 
-\series bold
-comportamiento conjuntivo
-\series default
- (se le puede aplicar una 
-\begin_inset Formula $\alpha$
-\end_inset
-
--fórmula) o 
-\series bold
-disyuntivo
-\series default
- (se le puede aplicar una 
-\begin_inset Formula $\beta$
-\end_inset
-
--fórmula), o ser un literal.
- Para cada rama del árbol:
-\end_layout
-
-\begin_layout Enumerate
-Seleccionamos una oración que no sea un literal, preferiblemente con comportamie
-nto conjuntivo.
-\end_layout
-
-\begin_layout Enumerate
-Si no encontramos ninguna, el nodo es un nodo hoja.
- Lo marcamos como 
-\series bold
-cerrado
-\series default
- si contiene un literal y su contrario, de lo contrario como 
-\series bold
-abierto
-\series default
-.
-\end_layout
-
-\begin_layout Enumerate
-Si tiene comportamiento conjuntivo, aplicamos la 
-\begin_inset Formula $\alpha$
-\end_inset
-
--fórmula correspondiente y dibujamos una rama con la etiqueta 
-\begin_inset Formula $\alpha:\text{(nom. de fórmula)}$
-\end_inset
-
- y el nodo resultado de sustituir 
-\begin_inset Formula $\alpha,\phi_{1},\dots,\phi_{n}$
-\end_inset
-
- por 
-\begin_inset Formula $\alpha_{1},\alpha_{2},\phi_{1},\dots,\phi_{n}$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Enumerate
-Si tiene comportamiento disyuntivo, aplicamos la 
-\begin_inset Formula $\beta$
-\end_inset
-
--fórmula correspondiente y dibujamos dos ramas.
- La división se marca con la etiqueta 
-\begin_inset Formula $\beta:\text{(nom. de fórmula)}$
-\end_inset
-
- y los nodos son los resultantes de sustituir 
-\begin_inset Formula $\beta,\phi_{1},\dots,\phi_{n}$
-\end_inset
-
- por 
-\begin_inset Formula $\beta_{1},\phi_{1},\dots,\phi_{n}$
-\end_inset
-
- y 
-\begin_inset Formula $\beta_{2},\phi_{1},\dots,\phi_{n}$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Standard
-\align center
-\begin_inset Tabular
-<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/logic/n4.lyx b/logic/n4.lyx
deleted file mode 100644
index 3796419..0000000
--- a/logic/n4.lyx
+++ /dev/null
@@ -1,402 +0,0 @@
-#LyX 2.3 created this file. For more info see http://www.lyx.org/
-\lyxformat 544
-\begin_document
-\begin_header
-\save_transient_properties true
-\origin unavailable
-\textclass book
-\use_default_options true
-\maintain_unincluded_children false
-\language spanish
-\language_package default
-\inputencoding auto
-\fontencoding global
-\font_roman "default" "default"
-\font_sans "default" "default"
-\font_typewriter "default" "default"
-\font_math "auto" "auto"
-\font_default_family default
-\use_non_tex_fonts false
-\font_sc false
-\font_osf false
-\font_sf_scale 100 100
-\font_tt_scale 100 100
-\use_microtype false
-\use_dash_ligatures true
-\graphics default
-\default_output_format default
-\output_sync 0
-\bibtex_command default
-\index_command default
-\paperfontsize default
-\spacing single
-\use_hyperref false
-\papersize default
-\use_geometry false
-\use_package amsmath 1
-\use_package amssymb 1
-\use_package cancel 1
-\use_package esint 1
-\use_package mathdots 1
-\use_package mathtools 1
-\use_package mhchem 1
-\use_package stackrel 1
-\use_package stmaryrd 1
-\use_package undertilde 1
-\cite_engine basic
-\cite_engine_type default
-\biblio_style plain
-\use_bibtopic false
-\use_indices false
-\paperorientation portrait
-\suppress_date false
-\justification true
-\use_refstyle 1
-\use_minted 0
-\index Index
-\shortcut idx
-\color #008000
-\end_index
-\secnumdepth 3
-\tocdepth 3
-\paragraph_separation indent
-\paragraph_indentation default
-\is_math_indent 0
-\math_numbering_side default
-\quotes_style swiss
-\dynamic_quotes 0
-\papercolumns 1
-\papersides 1
-\paperpagestyle default
-\tracking_changes false
-\output_changes false
-\html_math_output 0
-\html_css_as_file 0
-\html_be_strict false
-\end_header
-
-\begin_body
-
-\begin_layout Standard
-Las expresiones, numeradas, están dentro de una caja, que se representa
- con los tres bordes de arriba, abajo y a la izquierda (a la derecha del
- número de línea).
- La caja principal no se suele representar.
- Si se usa una 
-\emph on
-Hipótesis
-\emph default
-, se crea una nueva caja (dentro de otra), y en cada caja las 
-\emph on
-Premisas
-\emph default
- o 
-\emph on
-Hipótesis
-\emph default
- van al principio y la última línea es la conclusión.
- Cada caja representa una deducción (
-\begin_inset Formula $\vdash$
-\end_inset
-
-).
-\end_layout
-
-\begin_layout Section
-Reglas
-\end_layout
-
-\begin_layout Standard
-\align center
-\begin_inset Tabular
-<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/logic/n5.lyx b/logic/n5.lyx
deleted file mode 100644
index e887da2..0000000
--- a/logic/n5.lyx
+++ /dev/null
@@ -1,660 +0,0 @@
-#LyX 2.3 created this file. For more info see http://www.lyx.org/
-\lyxformat 544
-\begin_document
-\begin_header
-\save_transient_properties true
-\origin unavailable
-\textclass book
-\use_default_options true
-\maintain_unincluded_children false
-\language spanish
-\language_package default
-\inputencoding auto
-\fontencoding global
-\font_roman "default" "default"
-\font_sans "default" "default"
-\font_typewriter "default" "default"
-\font_math "auto" "auto"
-\font_default_family default
-\use_non_tex_fonts false
-\font_sc false
-\font_osf false
-\font_sf_scale 100 100
-\font_tt_scale 100 100
-\use_microtype false
-\use_dash_ligatures true
-\graphics default
-\default_output_format default
-\output_sync 0
-\bibtex_command default
-\index_command default
-\paperfontsize default
-\spacing single
-\use_hyperref false
-\papersize default
-\use_geometry false
-\use_package amsmath 1
-\use_package amssymb 1
-\use_package cancel 1
-\use_package esint 1
-\use_package mathdots 1
-\use_package mathtools 1
-\use_package mhchem 1
-\use_package stackrel 1
-\use_package stmaryrd 1
-\use_package undertilde 1
-\cite_engine basic
-\cite_engine_type default
-\biblio_style plain
-\use_bibtopic false
-\use_indices false
-\paperorientation portrait
-\suppress_date false
-\justification true
-\use_refstyle 1
-\use_minted 0
-\index Index
-\shortcut idx
-\color #008000
-\end_index
-\secnumdepth 3
-\tocdepth 3
-\paragraph_separation indent
-\paragraph_indentation default
-\is_math_indent 0
-\math_numbering_side default
-\quotes_style swiss
-\dynamic_quotes 0
-\papercolumns 1
-\papersides 1
-\paperpagestyle default
-\tracking_changes false
-\output_changes false
-\html_math_output 0
-\html_css_as_file 0
-\html_be_strict false
-\end_header
-
-\begin_body
-
-\begin_layout Section
-Conjuntos
-\end_layout
-
-\begin_layout Standard
-Una 
-\series bold
-categoría
-\series default
- o 
-\series bold
-conjunto
-\series default
- es una colección no ordenada de 
-\series bold
-elementos
-\series default
-.
- Se dice que un elemento 
-\begin_inset Formula $x$
-\end_inset
-
- pertenece al conjunto 
-\begin_inset Formula $C$
-\end_inset
-
-, y se representa como 
-\begin_inset Formula $x\in C$
-\end_inset
-
- (negación: 
-\begin_inset Formula $x\notin C$
-\end_inset
-
-) o 
-\begin_inset Formula $C(x)$
-\end_inset
-
-.
- Podemos definir un conjunto por extensión (
-\begin_inset Formula $C=\{x_{1},x_{2},\dots\}$
-\end_inset
-
-), intensión (
-\begin_inset Formula $C=\{x|P(x)\}$
-\end_inset
-
-) o recursión (
-\begin_inset Formula $C=\{x|R(x)\}$
-\end_inset
-
-).
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Igualdad:
-\series default
- 
-\begin_inset Formula $A=B:\iff(x\in A\iff x\in B)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Inclusión:
-\series default
- 
-\begin_inset Formula $A\subseteq B:\iff(x\in A\implies x\in B)$
-\end_inset
-
- (negación: 
-\begin_inset Formula $A\nsubseteq B$
-\end_inset
-
-).
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Inclusión estricta:
-\series default
- 
-\begin_inset Formula $A\subsetneq B:\iff(A\subseteq B\text{ y }A\neq B$
-\end_inset
-
-).
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Conjunto total
-\series default
- o 
-\series bold
-universo:
-\series default
- 
-\begin_inset Formula ${\cal U}$
-\end_inset
-
-, el mayor conjunto que podemos considerar para un estudio.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Conjunto vacío:
-\series default
- 
-\begin_inset Formula $\emptyset=\{\}$
-\end_inset
-
-, sin elementos.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Partes:
-\series default
- 
-\begin_inset Formula ${\cal P}(X)=\{A|A\subseteq X\}$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Unión:
-\series default
- 
-\begin_inset Formula $A\cup B:=\{x|x\in A\text{ ó }x\in B\}$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Intersección:
-\series default
- 
-\begin_inset Formula $A\cap B:=\{x|x\in A\text{ y }x\in B\}$
-\end_inset
-
-.
- Si 
-\begin_inset Formula $A\cap B=\emptyset$
-\end_inset
-
-, 
-\begin_inset Formula $A$
-\end_inset
-
- y 
-\begin_inset Formula $B$
-\end_inset
-
- son 
-\series bold
-disjuntos
-\series default
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Diferencia:
-\series default
- 
-\begin_inset Formula $A-B:=A\backslash B:=\{x|x\in A\text{ y }x\notin B\}$
-\end_inset
-
-
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Complemento:
-\series default
- 
-\begin_inset Formula $\overline{A}:=A^{\complement}:={\cal U}\backslash A$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Standard
-Un 
-\series bold
-diagrama de Euler
-\series default
- representa los conjuntos como círculos bien unos dentro de otros, separados
- o intersecados, indicando de esta forma sus relaciones.
- Un 
-\series bold
-diagrama de Venn
-\series default
- representa los conjuntos como círculos todos intersecados entre sí, con
- las partes no vacías sombreadas.
-\end_layout
-
-\begin_layout Standard
-Una 
-\series bold
-familia de conjuntos
-\series default
- 
-\begin_inset Formula ${\cal A}$
-\end_inset
-
- es un conjunto formado solo por conjuntos, y es una 
-\series bold
-partición
-\series default
- de 
-\begin_inset Formula $A$
-\end_inset
-
- si y sólo si 
-\begin_inset Formula $\bigcup{\cal A}=A$
-\end_inset
-
- y si para todo 
-\begin_inset Formula $B,C\in{\cal A}$
-\end_inset
-
- con 
-\begin_inset Formula $B\neq C$
-\end_inset
-
- se tiene que 
-\begin_inset Formula $B\cap C=\emptyset$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Section
-Sintaxis
-\end_layout
-
-\begin_layout Standard
-Extensión de la lógica proposicional.
- Las proposiciones atómicas tienen la forma 
-\begin_inset Formula $P(x)$
-\end_inset
-
-, donde 
-\begin_inset Formula $P$
-\end_inset
-
- es una categoría y 
-\begin_inset Formula $x$
-\end_inset
-
- una variable (ambas conjuntos de letras latinas), y se leen 
-\begin_inset Quotes cld
-\end_inset
-
-
-\begin_inset Formula $x$
-\end_inset
-
- es 
-\begin_inset Formula $P$
-\end_inset
-
-
-\begin_inset Quotes crd
-\end_inset
-
-.
- Además, se añaden los cuantificadores 
-\begin_inset Formula $\forall x$
-\end_inset
-
- (para todo 
-\begin_inset Formula $x$
-\end_inset
-
-) y 
-\begin_inset Formula $\exists x$
-\end_inset
-
- (existe 
-\begin_inset Formula $x$
-\end_inset
-
-), donde 
-\begin_inset Formula $x$
-\end_inset
-
- puede ser cualquier variable.
- Estos tienen la misma prioridad que la negación.
- Las proposiciones compuestas se forman mediante cuatro 
-\series bold
-formas normales:
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Universal afirmativa:
-\series default
- 
-\begin_inset Formula $\forall x(P(x)\rightarrow Q(x))$
-\end_inset
-
-; 
-\begin_inset Quotes cld
-\end_inset
-
-todo 
-\begin_inset Formula $P$
-\end_inset
-
- es 
-\begin_inset Formula $Q$
-\end_inset
-
-
-\begin_inset Quotes crd
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Universal negativa:
-\series default
- 
-\begin_inset Formula $\forall x(P(x)\rightarrow\neg Q(x))$
-\end_inset
-
-; 
-\begin_inset Quotes cld
-\end_inset
-
-ningún 
-\begin_inset Formula $P$
-\end_inset
-
- es 
-\begin_inset Formula $Q$
-\end_inset
-
-
-\begin_inset Quotes crd
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Existencial afirmativa:
-\series default
- 
-\begin_inset Formula $\exists x(P(x)\land Q(x))$
-\end_inset
-
-; 
-\begin_inset Quotes cld
-\end_inset
-
-algún 
-\begin_inset Formula $P$
-\end_inset
-
- es 
-\begin_inset Formula $Q$
-\end_inset
-
-
-\begin_inset Quotes crd
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Existencial negativa:
-\series default
- 
-\begin_inset Formula $\exists x(P(x)\land\neg Q(x))$
-\end_inset
-
-; 
-\begin_inset Quotes cld
-\end_inset
-
-algún 
-\begin_inset Formula $P$
-\end_inset
-
- no es 
-\begin_inset Formula $Q$
-\end_inset
-
-
-\begin_inset Quotes crd
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Section
-Evaluación
-\end_layout
-
-\begin_layout Standard
-Para evaluar una proposición en LC interpretada en un mundo 
-\begin_inset Formula ${\cal M}$
-\end_inset
-
-:
-\end_layout
-
-\begin_layout Enumerate
-Definimos 
-\begin_inset Formula ${\cal U}$
-\end_inset
-
- como el conjunto de todos los elementos que aparecen en 
-\begin_inset Formula ${\cal M}$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Enumerate
-Identificamos cada categoría 
-\begin_inset Formula $P$
-\end_inset
-
- con un conjunto 
-\begin_inset Formula $P_{{\cal M}}$
-\end_inset
-
- del mundo.
- El resultado es la 
-\series bold
-interpretación
-\series default
- 
-\begin_inset Formula $I=\{P\mapsto P_{{\cal M}},\dots\}$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Enumerate
-Evaluamos el valor de verdad de la proposición a partir de la interpretación.
- Para ello:
-\end_layout
-
-\begin_deeper
-\begin_layout Enumerate
-Si encontramos un 
-\begin_inset Formula $\forall x\alpha[x]$
-\end_inset
-
-, decimos que esto es verdad si para cualquier 
-\begin_inset Formula $x\looparrowright d$
-\end_inset
-
- se cumple 
-\begin_inset Formula $V(\alpha[d])=V$
-\end_inset
-
-.
- Aquí, 
-\begin_inset Formula $\alpha[d]\equiv\{\alpha[x]\}_{d/x}$
-\end_inset
-
- el resultado de aplicar la 
-\series bold
-sustitución
-\series default
- 
-\begin_inset Formula $\{d/x\}$
-\end_inset
-
-.
- Entonces comprobamos 
-\begin_inset Formula $V(\alpha[d])$
-\end_inset
-
- para todo 
-\begin_inset Formula $x\looparrowright d$
-\end_inset
-
- (
-\series bold
-asignación
-\series default
-) con 
-\begin_inset Formula $d\in{\cal U}$
-\end_inset
-
- hasta encontrar un caso donde 
-\begin_inset Formula $V(\alpha[d])=F$
-\end_inset
-
- (con lo que 
-\begin_inset Formula $V(\forall x\alpha[x])=F$
-\end_inset
-
-) o llegar a que en todos 
-\begin_inset Formula $V(\alpha[d])=V$
-\end_inset
-
- (con lo que 
-\begin_inset Formula $V(\forall x\alpha[x])=V$
-\end_inset
-
-).
-\end_layout
-
-\begin_layout Enumerate
-Si encontramos un 
-\begin_inset Formula $\exists x\alpha[x]$
-\end_inset
-
- decimos que esto es verdad si encontramos un 
-\begin_inset Formula $x\looparrowright d$
-\end_inset
-
- para el que 
-\begin_inset Formula $V(\alpha[d])=V$
-\end_inset
-
-.
- Entonces comprobamos 
-\begin_inset Formula $V(\alpha[d])$
-\end_inset
-
- para todo 
-\begin_inset Formula $x\looparrowright d$
-\end_inset
-
- con 
-\begin_inset Formula $d\in{\cal U}$
-\end_inset
-
- hasta encontrar un caso donde 
-\begin_inset Formula $V(\alpha[d])=V$
-\end_inset
-
- (con lo que 
-\begin_inset Formula $V(\exists x\alpha[x])=V$
-\end_inset
-
-) o llegar a que todos son falsos (con lo que 
-\begin_inset Formula $V(\exists x\alpha[x])=F$
-\end_inset
-
-).
-\end_layout
-
-\end_deeper
-\end_body
-\end_document
diff --git a/logic/n6.lyx b/logic/n6.lyx
deleted file mode 100644
index f89c446..0000000
--- a/logic/n6.lyx
+++ /dev/null
@@ -1,1406 +0,0 @@
-#LyX 2.3 created this file. For more info see http://www.lyx.org/
-\lyxformat 544
-\begin_document
-\begin_header
-\save_transient_properties true
-\origin unavailable
-\textclass book
-\use_default_options true
-\maintain_unincluded_children false
-\language spanish
-\language_package default
-\inputencoding auto
-\fontencoding global
-\font_roman "default" "default"
-\font_sans "default" "default"
-\font_typewriter "default" "default"
-\font_math "auto" "auto"
-\font_default_family default
-\use_non_tex_fonts false
-\font_sc false
-\font_osf false
-\font_sf_scale 100 100
-\font_tt_scale 100 100
-\use_microtype false
-\use_dash_ligatures true
-\graphics default
-\default_output_format default
-\output_sync 0
-\bibtex_command default
-\index_command default
-\paperfontsize default
-\spacing single
-\use_hyperref false
-\papersize default
-\use_geometry false
-\use_package amsmath 1
-\use_package amssymb 1
-\use_package cancel 1
-\use_package esint 1
-\use_package mathdots 1
-\use_package mathtools 1
-\use_package mhchem 1
-\use_package stackrel 1
-\use_package stmaryrd 1
-\use_package undertilde 1
-\cite_engine basic
-\cite_engine_type default
-\biblio_style plain
-\use_bibtopic false
-\use_indices false
-\paperorientation portrait
-\suppress_date false
-\justification true
-\use_refstyle 1
-\use_minted 0
-\index Index
-\shortcut idx
-\color #008000
-\end_index
-\secnumdepth 3
-\tocdepth 3
-\paragraph_separation indent
-\paragraph_indentation default
-\is_math_indent 0
-\math_numbering_side default
-\quotes_style swiss
-\dynamic_quotes 0
-\papercolumns 1
-\papersides 1
-\paperpagestyle default
-\tracking_changes false
-\output_changes false
-\html_math_output 0
-\html_css_as_file 0
-\html_be_strict false
-\end_header
-
-\begin_body
-
-\begin_layout Section
-Relaciones
-\end_layout
-
-\begin_layout Standard
-La lógica de primer orden (L1) extiende la lógica categórica permitiendo
- expresar relaciones fuera de las formas normales y relaciones de varios
- objetos.
- Podemos distinguir:
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Categorías:
-\series default
- 
-\begin_inset Quotes cld
-\end_inset
-
-
-\begin_inset Formula $x$
-\end_inset
-
- es 
-\begin_inset Formula $P$
-\end_inset
-
-
-\begin_inset Quotes crd
-\end_inset
-
-, 
-\begin_inset Formula $x\in P$
-\end_inset
-
-, 
-\begin_inset Formula $P(r)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Relaciones binarias:
-\series default
- 
-\begin_inset Quotes cld
-\end_inset
-
-
-\begin_inset Formula $x$
-\end_inset
-
- e 
-\begin_inset Formula $y$
-\end_inset
-
- son 
-\begin_inset Formula $R$
-\end_inset
-
-
-\begin_inset Quotes crd
-\end_inset
-
-, 
-\begin_inset Quotes cld
-\end_inset
-
-
-\begin_inset Formula $x$
-\end_inset
-
- se relaciona con 
-\begin_inset Formula $y$
-\end_inset
-
-
-\begin_inset Quotes crd
-\end_inset
-
-, 
-\begin_inset Formula $(x,y)\in R$
-\end_inset
-
-, 
-\begin_inset Formula $R(x,y)$
-\end_inset
-
-, 
-\begin_inset Formula $xRy$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Relaciones
-\series default
- de cualquier orden: 
-\begin_inset Formula $(x_{1},\dots,x_{n})\in S$
-\end_inset
-
-, 
-\begin_inset Formula $S(x_{1},\dots,x_{n})$
-\end_inset
-
-.
- Se dice que 
-\begin_inset Formula $S$
-\end_inset
-
- tiene 
-\series bold
-aridad
-\series default
- 
-\begin_inset Formula $n$
-\end_inset
-
-, o que es una relación 
-\series bold
-
-\begin_inset Formula $n$
-\end_inset
-
--aria
-\series default
-, lo que se representa por 
-\begin_inset Formula $S/n$
-\end_inset
-
-.
- En general, 
-\begin_inset Formula $Q$
-\end_inset
-
- es una relación 
-\begin_inset Formula $n$
-\end_inset
-
--aria entre 
-\begin_inset Formula $A_{1},\dots,A_{n}$
-\end_inset
-
- si 
-\begin_inset Formula $Q\subseteq\prod_{i=1}^{n}A_{i}$
-\end_inset
-
-.
- Si 
-\begin_inset Formula $\forall i,A_{i}=A$
-\end_inset
-
-, entonces 
-\begin_inset Formula $\prod_{i=1}^{n}A_{i}=A^{n}$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Standard
-En relaciones con aridad 
-\begin_inset Formula $n\geq2$
-\end_inset
-
-, se define el 
-\series bold
-dominio
-\series default
- como 
-\begin_inset Formula $\text{Dom}(R)=\{(x_{1},\dots,x_{n-1})|\exists x_{n}:(x_{1},\dots,x_{n})\in R\}$
-\end_inset
-
- (si la aridad es 
-\begin_inset Formula $2$
-\end_inset
-
-, entonces 
-\begin_inset Formula $\text{Dom}(R)=\{x|\exists y:xRy\}$
-\end_inset
-
-), y el 
-\series bold
-rango
-\series default
- como 
-\begin_inset Formula $\text{Ran}(R)=\{x_{n}|\exists(x_{1},\dots,x_{n-1}):(x_{1},\dots,x_{n})\in R\}$
-\end_inset
-
- (si la aridad es 
-\begin_inset Formula $2$
-\end_inset
-
-, entonces 
-\begin_inset Formula $\text{Ran}(R)=\{y|\exists x:xRy\}$
-\end_inset
-
-.
- El 
-\series bold
-campo
-\series default
- de 
-\begin_inset Formula $R$
-\end_inset
-
- se define como 
-\begin_inset Formula $\text{Campo}(R)=\text{Dom}(R)\cup\text{Ran}(R)$
-\end_inset
-
-.
- Representaciones:
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Cartesiana:
-\series default
- Similar a una función, con el conjunto inicial en el eje horizontal.
- Se marcan los puntos que están en 
-\begin_inset Formula $R$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Tabular:
-\series default
- Como la cartesiana pero en una tabla.
- En cada celda se pone un 
-\begin_inset Formula $1$
-\end_inset
-
- si el producto de tipos está en 
-\begin_inset Formula $R$
-\end_inset
-
-, un 
-\begin_inset Formula $0$
-\end_inset
-
- si no está y se deja en blanco si no lo sabemos.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Mediante digrafo:
-\series default
- Se representa a la izquierda el conjunto inicial y a la derecha el final,
- y las relaciones se representan con flechas entre elementos de cada.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Grafo dirigido:
-\series default
- Se representa 
-\begin_inset Formula ${\cal U}$
-\end_inset
-
- y se indican las relaciones binarias con flechas.
-\end_layout
-
-\begin_layout Standard
-Una relación 
-\begin_inset Formula $n$
-\end_inset
-
--aria 
-\begin_inset Formula $f$
-\end_inset
-
- es una 
-\series bold
-función
-\series default
- si y sólo si para cada elemento 
-\begin_inset Formula $x\in\text{Dom}(f)$
-\end_inset
-
- existe un único 
-\begin_inset Formula $y\in\text{Ran}(f)$
-\end_inset
-
- que se relacione con él.
- Se escribe 
-\begin_inset Formula $f(x)=y$
-\end_inset
-
-, y la función se representa como 
-\begin_inset Formula $f:\prod_{i=1}^{n-1}A_{i}\rightarrow A_{n}$
-\end_inset
-
-.
- Es 
-\series bold
-inyectiva
-\series default
- si 
-\begin_inset Formula $f(x)=f(x')\implies x=x'$
-\end_inset
-
-, 
-\series bold
-suprayectiva
-\series default
- si 
-\begin_inset Formula $\text{Ran}(f)=A_{n}$
-\end_inset
-
- y 
-\series bold
-biyectiva
-\series default
- si es inyectiva y suprayectiva.
- Definimos la aridad de 
-\begin_inset Formula $f$
-\end_inset
-
- como función como 
-\begin_inset Formula $n-1$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Standard
-\begin_inset Note Comment
-status open
-
-\begin_layout Plain Layout
-Tipos de relaciones:
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Reflexiva:
-\series default
- 
-\begin_inset Formula $\forall a\in A,aRa$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Irreflexiva:
-\series default
- 
-\begin_inset Formula $\forall a\in A,a\not Ra$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Serial:
-\series default
- 
-\begin_inset Formula $\forall a\in A,\exists b\in A:aRb$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Simétrica:
-\series default
- 
-\begin_inset Formula $\forall a,b\in A,(aRb\implies bRa)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Asimétrica:
-\series default
- 
-\begin_inset Formula $\forall a,b\in A,(aRb\implies b\not Ra)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Antisimétrica:
-\series default
- 
-\begin_inset Formula $\forall a,b\in A,(aRb\land bRa\implies a=b)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Transitiva:
-\series default
- 
-\begin_inset Formula $\forall a,b,c\in A,(aRb\land bRc\implies aRc)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Intransitiva:
-\series default
- 
-\begin_inset Formula $\forall a,b,c\in A,(aRb\land bRc\implies a\not Rc)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Negativamente transitiva:
-\series default
- 
-\begin_inset Formula $\forall a,b,c\in A,(a\not Rb\land b\not Rc\implies a\not Rc)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Completa:
-\series default
- 
-\begin_inset Formula $\forall a,b\in A,(aRb\lor bRa)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Euclídea:
-\series default
- 
-\begin_inset Formula $\forall a,b,c\in A,(aRb\land aRc\implies bRc)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Incestuosa:
-\series default
- 
-\begin_inset Formula $\forall a,b,c\in A,(aRb\land aRc\implies\exists d\in A:(bRd\land cRd))$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Plain Layout
-Dada 
-\begin_inset Formula $R\subseteq A\times B$
-\end_inset
-
-, su 
-\series bold
-relación inversa
-\series default
- es 
-\begin_inset Formula $R^{-1}$
-\end_inset
-
- con 
-\begin_inset Formula $xR^{-1}y:\iff yRx$
-\end_inset
-
-.
- Dada 
-\begin_inset Formula $R\subseteq A\times A$
-\end_inset
-
-:
-\end_layout
-
-\begin_layout Itemize
-Su 
-\series bold
-relación complementaria
-\series default
- es 
-\begin_inset Formula $R^{\complement}$
-\end_inset
-
- con 
-\begin_inset Formula $xR^{\complement}y:\iff x\not Ry$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-Su 
-\series bold
-relación simétrica
-\series default
- es 
-\begin_inset Formula $\overline{R}=R^{-1}$
-\end_inset
-
- con 
-\begin_inset Formula $x\overline{R}y:\iff yRx$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-Su 
-\series bold
-relación dual
-\series default
- es 
-\begin_inset Formula $R^{d}$
-\end_inset
-
- con 
-\begin_inset Formula $aR^{d}b:\iff b\not Ra$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Plain Layout
-Una relación de equivalencia es aquella reflexiva, simétrica y transitiva.
- Sea 
-\begin_inset Formula $(A,\sim)$
-\end_inset
-
- de equivalencia, podemos definir la clase de equivalencia de 
-\begin_inset Formula $x$
-\end_inset
-
-, 
-\begin_inset Formula $[x]$
-\end_inset
-
-, como el conjunto de todos los elementos que se relacionan con 
-\begin_inset Formula $[x]$
-\end_inset
-
-.
- 
-\begin_inset Formula $y\in[x]\implies[y]=[x]$
-\end_inset
-
-, y decimos que 
-\begin_inset Formula $y$
-\end_inset
-
- es un representante de la clase.
- El conjunto cociente es el formado por todas las clases de equivalencia,
- y se escribe 
-\begin_inset Formula $A/\sim=\{[x]|x\in A\}$
-\end_inset
-
-.
-\end_layout
-
-\end_inset
-
-
-\end_layout
-
-\begin_layout Section
-Sintaxis
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Proposición atómica:
-\series default
- 
-\begin_inset Formula $V$
-\end_inset
-
-, 
-\begin_inset Formula $F$
-\end_inset
-
- o un predicado.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Predicado:
-\series default
- Secuencia de letras latinas que representa una relación, seguida de una
- serie de términos: 
-\begin_inset Formula $R(t_{1},\dots,t_{n})$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Término:
-\series default
- Constante que representa un objeto definido, variable o función.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Constante:
-\series default
- Secuencia de letras latinas que representa a un objeto definido (salvo
- 
-\begin_inset Formula $V$
-\end_inset
-
- y 
-\begin_inset Formula $F$
-\end_inset
-
-).
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Variable:
-\series default
- Secuencia de letras latinas que representa a un objeto indefinido.
- Puede estar 
-\series bold
-ligada
-\series default
- a un cuantificador, y entonces es igual al resto de variables ligadas al
- mismo, o 
-\series bold
-libre
-\series default
-, en cuyo caso puede representar cualquier cosa.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Función:
-\series default
- Secuencia de letras latinas que representa una función, seguida de una
- serie de términos: 
-\begin_inset Formula $f(t_{1},\dots,t_{n})$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Standard
-La construcción de f.b.f es igual que en L0, pero cambiando la forma de las
- proposiciones atómicas y añadiendo que si 
-\begin_inset Formula $\alpha$
-\end_inset
-
- es f.b.f.
- también lo son 
-\begin_inset Formula $(\forall x\alpha)$
-\end_inset
-
- y 
-\begin_inset Formula $(\exists x\alpha)$
-\end_inset
-
-.
- Una f.b.f.
- es 
-\series bold
-cerrada
-\series default
- si todas las variables están ligadas y 
-\series bold
-abierta
-\series default
- en otro caso.
-\end_layout
-
-\begin_layout Section
-Interpretación y asignación
-\end_layout
-
-\begin_layout Standard
-Una 
-\series bold
-interpretación
-\series default
- de 
-\begin_inset Formula $\alpha$
-\end_inset
-
- en un 
-\series bold
-mundo
-\series default
- 
-\begin_inset Formula $\mathbb{M}$
-\end_inset
-
- es una cuaterna 
-\begin_inset Formula ${\cal I}_{\alpha}=(\mathbb{D},{\cal C}_{\mathbb{D}},{\cal F}_{\mathbb{D}},{\cal R}_{\mathbb{D}})$
-\end_inset
-
- donde 
-\begin_inset Formula $\mathbb{D}$
-\end_inset
-
- es un conjunto no vacío de objetos, llamado dominio, 
-\begin_inset Formula ${\cal C}_{\mathbb{D}}$
-\end_inset
-
- es un conjunto de objetos concretos (
-\begin_inset Formula ${\cal C_{\alpha}\mapsto{\cal C}_{\mathbb{D}}}$
-\end_inset
-
-), 
-\begin_inset Formula ${\cal F}_{\mathbb{D}}$
-\end_inset
-
- de funciones concretas (
-\begin_inset Formula $f_{\alpha}\mapsto f_{\mathbb{D}}$
-\end_inset
-
-) y 
-\begin_inset Formula ${\cal R}_{\mathbb{D}}$
-\end_inset
-
- de relaciones concretas (
-\begin_inset Formula $R_{\alpha}\mapsto R_{\mathbb{D}}$
-\end_inset
-
-).
- La 
-\series bold
-signatura
-\series default
- es el conjunto de todos los predicados y funciones, indicando su aridad.
-\end_layout
-
-\begin_layout Standard
-Una asignación de variables es una función 
-\begin_inset Formula $\sigma_{{\cal I}_{\alpha}}:{\cal V}\rightarrow\mathbb{D}$
-\end_inset
-
- que relaciona cada variable de 
-\begin_inset Formula $\alpha$
-\end_inset
-
- con un elemento del dominio, y definimos 
-\begin_inset Formula $\sigma_{{\cal I}_{\alpha}|x\looparrowright d}$
-\end_inset
-
- a la asignación definida igual que 
-\begin_inset Formula $\sigma_{{\cal I}_{\alpha}}$
-\end_inset
-
- pero asignando a 
-\begin_inset Formula $x$
-\end_inset
-
- el objeto 
-\begin_inset Formula $d$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Standard
-Una 
-\series bold
-asignación de valores de verdad
-\series default
- 
-\begin_inset Formula $v_{\sigma_{{\cal I}_{\alpha}}}:{\cal P_{\alpha}\rightarrow\mathbb{B}}$
-\end_inset
-
- asigna un valor de verdad a cada elemento atómico de 
-\begin_inset Formula $\alpha$
-\end_inset
-
-.
- Así, 
-\begin_inset Formula $v(R_{\alpha}(t_{1},\dots,t_{n}))=V\iff(d_{1},\dots,d_{n})\in R_{\mathbb{D}}$
-\end_inset
-
-, donde si 
-\begin_inset Formula $t_{i}$
-\end_inset
-
- es constante entonces 
-\begin_inset Formula $d_{i}=t_{i}$
-\end_inset
-
-, si 
-\begin_inset Formula $t_{i}=f(x_{1},\dots,x_{n})$
-\end_inset
-
- entonces 
-\begin_inset Formula $d_{i}$
-\end_inset
-
- es el único 
-\begin_inset Formula $y$
-\end_inset
-
- tal que 
-\begin_inset Formula $(x_{1},\dots,x_{n},y)\in f$
-\end_inset
-
-, y si es variable entonces depende de la 
-\series bold
-asignación
-\series default
-.
-\end_layout
-
-\begin_layout Standard
-La 
-\series bold
-evaluación
-\series default
- de una oración 
-\begin_inset Formula $\alpha$
-\end_inset
-
- se hace igual que en LC, pero partiendo de esta asignación de valores de
- verdad.
- También se puede hacer mediante tablas de verdad, que en L1 sólo evalúan
- una interpretación a la vez:
-\end_layout
-
-\begin_layout Enumerate
-Se introduce una columna por variable, dividida en una fila por cada valor
- del dominio.
- Puede ser necesario considerar aquí todas las posibles combinaciones de
- variables.
-\end_layout
-
-\begin_layout Enumerate
-Se introduce una columna por cada función que aparece en la oración, y se
- evalúa de acuerdo al valor de la variable dado.
-\end_layout
-
-\begin_layout Enumerate
-Se introducen las filas correspondientes a la fórmula, indicando el orden
- de evaluación.
- Un cuantificador que no está dentro de otro ocupa la fila completa, pero
- su contenido se divide en una fila por cada posible asignación de la variable.
- Una vez se conoce el valor del cuantificador no es necesario evaluar el
- resto de asignaciones, pero es importante justificar los valores de verdad
- de los predicados (ejemplos: 
-\begin_inset Formula $V:(a,b)\in P_{{\cal M}}$
-\end_inset
-
-; 
-\begin_inset Formula $F:(c,a)\notin Q_{{\cal M}}$
-\end_inset
-
-).
-\end_layout
-
-\begin_layout Standard
-Este método es impráctico, por lo que no se usa.
-\end_layout
-
-\begin_layout Section
-Sustituciones
-\end_layout
-
-\begin_layout Standard
-Una 
-\series bold
-sustitución
-\series default
- es una expresión 
-\begin_inset Formula $s=\{t_{1}/v_{1},\dots,t_{n}/v_{n}\}$
-\end_inset
-
- que indica que toda ocurrencia de cada 
-\begin_inset Formula $v_{i}$
-\end_inset
-
- se debe sustituir por el término 
-\begin_inset Formula $t_{i}$
-\end_inset
-
-.
- Todas las sustituciones se hacen simultáneamente.
-\end_layout
-
-\begin_layout Standard
-Una 
-\series bold
-particularización por sustitución
-\series default
- consiste en sustituir sus variables por términos.
- Escribimos 
-\begin_inset Formula $Ps$
-\end_inset
-
- como la particularización de la expresión 
-\begin_inset Formula $P$
-\end_inset
-
- según la sustitución 
-\begin_inset Formula $s$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-En una 
-\series bold
-particularización básica
-\series default
-, los términos son constantes.
-\end_layout
-
-\begin_layout Itemize
-En una 
-\series bold
-particularización alfabética
-\series default
-, los términos son otras variables.
-\end_layout
-
-\begin_layout Standard
-
-\series bold
-Composición de sustituciones:
-\series default
- Dadas 
-\begin_inset Formula $s=\{a_{1}/x_{1},\dots,a_{n}/x_{n}\}$
-\end_inset
-
- y 
-\begin_inset Formula $t=\{b_{1}/y_{1},\dots,b_{m}/y_{m}\}$
-\end_inset
-
- con 
-\begin_inset Formula $X$
-\end_inset
-
- e 
-\begin_inset Formula $Y$
-\end_inset
-
- los conjuntos de variables sustituidas respectivamente según 
-\begin_inset Formula $s$
-\end_inset
-
- y 
-\begin_inset Formula $t$
-\end_inset
-
-, 
-\begin_inset Formula $s\cdot t=\{(a_{i}t)/x_{i}|x_{i}\neq a_{i}t\}\cup\{b_{i}/y_{i}|y_{i}\in Y\backslash X\}$
-\end_inset
-
-, donde 
-\begin_inset Formula $a_{i}t$
-\end_inset
-
- es la particularización de 
-\begin_inset Formula $a_{i}$
-\end_inset
-
- según 
-\begin_inset Formula $t$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Section
-Equivalencias
-\end_layout
-
-\begin_layout Standard
-\align center
-\begin_inset Tabular
-<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/logic/n7.lyx b/logic/n7.lyx
deleted file mode 100644
index b05b04e..0000000
--- a/logic/n7.lyx
+++ /dev/null
@@ -1,609 +0,0 @@
-#LyX 2.3 created this file. For more info see http://www.lyx.org/
-\lyxformat 544
-\begin_document
-\begin_header
-\save_transient_properties true
-\origin unavailable
-\textclass book
-\use_default_options true
-\maintain_unincluded_children false
-\language spanish
-\language_package default
-\inputencoding auto
-\fontencoding global
-\font_roman "default" "default"
-\font_sans "default" "default"
-\font_typewriter "default" "default"
-\font_math "auto" "auto"
-\font_default_family default
-\use_non_tex_fonts false
-\font_sc false
-\font_osf false
-\font_sf_scale 100 100
-\font_tt_scale 100 100
-\use_microtype false
-\use_dash_ligatures true
-\graphics default
-\default_output_format default
-\output_sync 0
-\bibtex_command default
-\index_command default
-\paperfontsize default
-\spacing single
-\use_hyperref false
-\papersize default
-\use_geometry false
-\use_package amsmath 1
-\use_package amssymb 1
-\use_package cancel 1
-\use_package esint 1
-\use_package mathdots 1
-\use_package mathtools 1
-\use_package mhchem 1
-\use_package stackrel 1
-\use_package stmaryrd 1
-\use_package undertilde 1
-\cite_engine basic
-\cite_engine_type default
-\biblio_style plain
-\use_bibtopic false
-\use_indices false
-\paperorientation portrait
-\suppress_date false
-\justification true
-\use_refstyle 1
-\use_minted 0
-\index Index
-\shortcut idx
-\color #008000
-\end_index
-\secnumdepth 3
-\tocdepth 3
-\paragraph_separation indent
-\paragraph_indentation default
-\is_math_indent 0
-\math_numbering_side default
-\quotes_style swiss
-\dynamic_quotes 0
-\papercolumns 1
-\papersides 1
-\paperpagestyle default
-\tracking_changes false
-\output_changes false
-\html_math_output 0
-\html_css_as_file 0
-\html_be_strict false
-\end_header
-
-\begin_body
-
-\begin_layout Standard
-Un 
-\series bold
-sistema deductivo
-\series default
- es un conjunto de axiomas y reglas de inferencia sintácticas (
-\begin_inset Formula $\vdash$
-\end_inset
-
-).
- Una 
-\series bold
-demostración
-\series default
- o 
-\series bold
-prueba formal
-\series default
- es una secuencia de conjuntos de fórmulas en las que cada fórmula es un
- axioma o puede obtenerse del conjunto anterior mediante una regla de inferencia.
- Cada elemento 
-\begin_inset Formula $\alpha$
-\end_inset
-
- del último conjunto de la secuencia se llama 
-\series bold
-teorema por deducción
-\series default
-, y se dice que 
-\begin_inset Formula $\alpha$
-\end_inset
-
- es 
-\series bold
-demostrable
-\series default
-, lo que escribimos como 
-\begin_inset Formula $\vdash\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Standard
-Un sistema deductivo en L0 y L1 es 
-\series bold
-sólido
-\series default
- si y sólo si 
-\begin_inset Formula $\vdash\alpha\implies\vDash\alpha$
-\end_inset
-
-, es decir, si cualquier conclusión 
-\series bold
-derivable
-\series default
- o 
-\series bold
-deducible 
-\series default
-a partir de las reglas es válida, y es 
-\series bold
-completo
-\series default
- cuando 
-\begin_inset Formula $\vDash\alpha\implies\vdash\alpha$
-\end_inset
-
-.
- Un conjunto de reglas es 
-\series bold
-inconsistente
-\series default
- si 
-\begin_inset Formula $\vdash\alpha\land\neg\alpha$
-\end_inset
-
-, y es 
-\series bold
-consistente
-\series default
- si no es inconsistente.
-\end_layout
-
-\begin_layout Standard
-Dada una oración 
-\begin_inset Formula $\alpha$
-\end_inset
-
- y un conjunto de oraciones 
-\begin_inset Formula ${\cal F}$
-\end_inset
-
-, 
-\begin_inset Formula $\vDash\alpha$
-\end_inset
-
- significa que 
-\begin_inset Formula $\alpha$
-\end_inset
-
- es válida y 
-\begin_inset Formula ${\cal F}\vDash\alpha$
-\end_inset
-
- significa que 
-\begin_inset Formula $\alpha$
-\end_inset
-
- es consecuencia lógica de 
-\begin_inset Formula ${\cal F}$
-\end_inset
-
-.
- Por su parte 
-\begin_inset Formula $\vdash\alpha$
-\end_inset
-
- significa que 
-\begin_inset Formula $\alpha$
-\end_inset
-
- es demostrable y 
-\begin_inset Formula ${\cal F}\vdash\alpha$
-\end_inset
-
- significa que 
-\begin_inset Formula $\alpha$
-\end_inset
-
- es deducible de 
-\begin_inset Formula ${\cal F}$
-\end_inset
-
-, y representa una 
-\series bold
-deducción
-\series default
- o 
-\series bold
-razonamiento
-\series default
-, donde 
-\begin_inset Formula $\alpha$
-\end_inset
-
- es la conclusión o 
-\series bold
-derivación
-\series default
- y las 
-\begin_inset Formula $\psi\in{\cal F}$
-\end_inset
-
- son las premisas, las fórmulas usadas para llegar a 
-\begin_inset Formula $\alpha$
-\end_inset
-
-.
- 
-\end_layout
-
-\begin_layout Standard
-Decimos que un conjunto de oraciones 
-\begin_inset Formula ${\cal T}$
-\end_inset
-
- es una 
-\series bold
-teoría
-\series default
- si 
-\begin_inset Formula $\forall\alpha({\cal T}\vDash\alpha\implies\alpha\in{\cal T})$
-\end_inset
-
-, y entonces cada 
-\begin_inset Formula $\alpha\in{\cal T}$
-\end_inset
-
- es un 
-\series bold
-teorema
-\series default
-.
- Una teoría es 
-\series bold
-axiomatizable
-\series default
- si existe un subconjunto 
-\begin_inset Formula ${\cal F}$
-\end_inset
-
- tal que 
-\begin_inset Formula ${\cal T}=\{\alpha|{\cal F}\vDash\alpha\}$
-\end_inset
-
-, y cada 
-\begin_inset Formula $\alpha\in{\cal F}$
-\end_inset
-
- es un 
-\series bold
-axioma
-\series default
-, y es 
-\series bold
-contradictoria
-\series default
- o 
-\series bold
-inconsistente
-\series default
- cuando 
-\begin_inset Formula ${\cal T}\vDash\alpha$
-\end_inset
-
- y 
-\begin_inset Formula ${\cal T}\vDash\neg\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Standard
-Una teoría es 
-\series bold
-decidible
-\series default
- si se puede determinar la consistencia o inconsistencia de una fórmula
- mediante un algoritmo; 
-\series bold
-semidecidible
-\series default
- si hay fórmulas cuya inconsistencia no puede ser probada algorítmicamente,
- e 
-\series bold
-indecidible
-\series default
- si no es posible crear un algoritmo que determine la consistencia o inconsisten
-cia de una fórmula.
-\end_layout
-
-\begin_layout Standard
-
-\series bold
-Hilbert
-\series default
- opinaba que todo sistema fundamental matemático debía ser consistente,
- completo y decidible, pero Kurt
-\series bold
- Gödel
-\series default
- demostró que ningún sistema capaz de representar los números naturales
- puede ser a la vez consistente y completo, y que la consistencia no puede
- probarse con los propios axiomas del sistema, por lo que habrá verdades
- que no se pueden demostrar.
- Alan 
-\series bold
-Turing
-\series default
-, por su parte, demostró que solo sistemas muy restrictivos son decidibles.
-\end_layout
-
-\begin_layout Standard
-Un sistema deductivo cumple el 
-\series bold
-teorema de la deducción
-\series default
- si verifica que, dado el conjunto 
-\begin_inset Formula ${\cal F}$
-\end_inset
-
- y las fórmulas 
-\begin_inset Formula $\alpha$
-\end_inset
-
- y 
-\begin_inset Formula $\beta$
-\end_inset
-
-, 
-\begin_inset Formula ${\cal F}\cup\{\alpha\}\vdash\beta\iff{\cal F}\vdash\alpha\rightarrow\beta$
-\end_inset
-
-.
- Así, 
-\begin_inset Formula ${\cal F}\cup\{\alpha_{1},\dots,\alpha_{n}\}\vdash\beta\iff{\cal F}\cup\{\alpha_{1},\dots,\alpha_{n-1}\}\vdash\alpha_{n}\rightarrow\beta\iff\dots\iff{\cal F}\vdash\alpha_{1}\rightarrow(\alpha_{2}\rightarrow\cdots(\alpha_{n}\rightarrow\beta)\cdots)$
-\end_inset
-
-.
- Este teorema simplifica mucho las demostraciones, si bien no se probó su
- corrección hasta 1930.
- No todos los sistemas cumplen en teorema de la deducción, si bien el Teorema
- de la Deducción Semántica (
-\begin_inset Formula ${\cal F}\cup\{a\}\vDash\beta\iff{\cal F}\vDash\alpha\rightarrow\beta$
-\end_inset
-
-) se cumple siempre.
- Decimos que 
-\begin_inset Formula ${\cal F}$
-\end_inset
-
- es 
-\series bold
-sintácticamente completo
-\series default
- si para todo 
-\begin_inset Formula $\alpha$
-\end_inset
-
-, 
-\begin_inset Formula ${\cal F}\vdash\alpha$
-\end_inset
-
- o 
-\begin_inset Formula ${\cal F}\vdash\neg\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Standard
-Un 
-\series bold
-razonamiento deductivo
-\series default
- es el que parte de unas hipótesis básicas para obtener unas consecuencias
- (
-\begin_inset Formula $\alpha\vDash\beta$
-\end_inset
-
-).
- Normalmente parte de premisas sobre aspectos generales para concluir aspectos
- particulares.
- La relación entre premisas y conclusión es de implicación (
-\begin_inset Formula $\alpha\vDash\beta\iff\vDash\alpha\rightarrow\beta$
-\end_inset
-
-).
- Algunos tipos de 
-\series bold
-demostración
-\series default
- deductiva (de 
-\begin_inset Formula $\vDash\alpha\rightarrow\beta$
-\end_inset
-
-):
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Vacía
-\series default
- de 
-\begin_inset Formula $\alpha\rightarrow\beta$
-\end_inset
-
-: 
-\begin_inset Formula $\forall v_{I},v(\alpha)=F$
-\end_inset
-
- (no se usa 
-\begin_inset Formula $\beta$
-\end_inset
-
-).
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Trivial
-\series default
-: 
-\begin_inset Formula $\forall v_{I},v(\beta)=V$
-\end_inset
-
- (no se usa 
-\begin_inset Formula $\alpha$
-\end_inset
-
-).
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Directa
-\series default
-: Probar que 
-\begin_inset Formula $\alpha\vDash\beta$
-\end_inset
-
- usando definiciones o teoremas ya probados, como el Modus Ponens.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Por contrarrecíproco
-\series default
-: 
-\begin_inset Formula $\alpha\rightarrow\beta\equiv\neg\beta\rightarrow\neg\alpha$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Por contradicción
-\series default
-: 
-\begin_inset Formula $\alpha\rightarrow\beta\equiv\alpha\land\neg\beta\rightarrow\gamma\land\neg\gamma$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Indirecta
-\series default
-: Si 
-\begin_inset Formula $\alpha\vDash\gamma$
-\end_inset
-
- y 
-\begin_inset Formula $\gamma\vDash\beta$
-\end_inset
-
- entonces 
-\begin_inset Formula $\alpha\vDash\beta$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Standard
-La 
-\series bold
-refutación por contraejemplo
-\series default
- consiste en buscar 
-\begin_inset Formula $a$
-\end_inset
-
- tal que 
-\begin_inset Formula $v(\alpha[a]\rightarrow\beta[a])=F$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Standard
-Un 
-\series bold
-razonamiento inductivo
-\series default
- consiste en obtener reglas generales a partir de casos particulares.
- Para ello se observan, registran y analizan hechos y se formulan leyes
- universales a modo de hipótesis o conjeturas, tras lo cual se diseñan experimen
-tos para ver que estas leyes se cumplen.
-\end_layout
-
-\begin_layout Standard
-La 
-\series bold
-inducción matemática
-\series default
-, sin embargo, se puede probar de forma deductiva, si bien esto requiere
- lógica de segundo orden.
- En 
-\begin_inset Formula $\mathbb{N}$
-\end_inset
-
-, para un 
-\begin_inset Formula $n_{0}\in\mathbb{N}$
-\end_inset
-
-, tenemos:
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Principio de inducción débil
-\series default
-: 
-\begin_inset Formula $\{P(n_{0})\}\cup\bigcup_{n\geq n_{0}}\{P(n)\rightarrow P(n+1)\}\vDash\forall n\geq n_{0},P(n)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Itemize
-
-\series bold
-Principio de inducción fuerte
-\series default
-: 
-\begin_inset Formula $\{P(n_{0})\}\cup\bigcup_{n\geq n_{0}}\{P(n_{0})\land\dots\land P(n)\rightarrow P(n+1)\}\vDash\forall n\geq n_{0},P(n)$
-\end_inset
-
-.
-\end_layout
-
-\begin_layout Standard
-El 
-\series bold
-principio de inducción estructural
-\series default
- para 
-\series bold
-demostración por recursión
-\series default
- es una generalización de la inducción y afirma que, dado un conjunto de
- elementos definido por recursión con una serie de casos base y reglas de
- recursión sobre estos, si una propiedad se cumple para cada caso base,
- y si en cada regla de recursión si la propiedad se cumple para los parámetros
- de entrada también se cumple para el elemento resultante de aplicarla,
- entonces esta propiedad la cumplen todos los elementos del conjunto.
-\end_layout
-
-\end_body
-\end_document