Mathematics">
L Ogica para La Computaci On: II) L Ogica CL Asica de Primer Orden
L Ogica para La Computaci On: II) L Ogica CL Asica de Primer Orden
L Ogica para La Computaci On: II) L Ogica CL Asica de Primer Orden
Este documento presenta la Lógica Clásica de Primer Orden. En él hemos puesto especial
énfasis en los aspectos algorı́tmicos, en definitiva, en presentar la lógica como el Cálculo de las
Ciencias de la Computación y, en particular, como la base matemática del software.
ii
Índice general
2. Modelos de Herbrand 51
2.1. Interpretaciones de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
2.2. Teorema de Herbrand y Semidecidibilidad de L1 . . . . . . . . . . . . . . . . . . 56
2.2.1. Árboles Semánticos en L1 . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
2.2.2. Teorema de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
2.3. Modelos Finitos y Modelos Infinitos . . . . . . . . . . . . . . . . . . . . . . . . . 65
2.3.1. Compacidad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
2.4. Indecidibilidad de L1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
2.5. Ejercicios . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
iii
iv ÍNDICE GENERAL
En el primer libro hemos contemplado el tipo más simple de lenguaje lógico, el de la lógica
proposicional clásica, la cual, a fin de establecer criterios sobre la exactitud de razonamientos,
formaliza la parte más elemental de nuestro lenguaje natural, es concretamente:
sólo se consideran las frases declarativas, llamadas proposiciones o enunciados, a las que es
posible considerar o bien verdaderas o bien falsas y ningún otro valor de verdad (es decir,
es bivaluada y admite el Principio del tercero excluido: A ∨ ¬A siempre es verdadera).
Este valor de verdad queda completamente determinado por el valor de verdad o falsedad
de los enunciados simples que la componen y por las partı́culas no, o, y, si . . . entonces,
si y sólo si, utilizadas como elementos de enlace (es decir, es veritativo-funcional).
p
q
r
1
2 CAPÍTULO 1. LÓGICA DE PRIMER ORDEN
Del mismo modo, la lógica proposicional clásica no basta para analizar la corrección de pro-
gramas respecto a una especificación formal. Por ejemplo, la corrección de un programa que
computa el mayor elemento de una lista de números enteros, requiere manejar expresiones del
tipo x < y. Esta expresión “predica” una determinada relación entre x e y, y su verdad o falsedad
depende de los valores de x y de y.
La insuficiencia de la lógica proposicional clásica, es decir, su escasa potencia expresiva, requiere
el desarrollo de una lógica más amplia que permita considerar válidos los razonamientos del tipo
anterior. Necesitamos una lógica que permita captar más detalles del lenguaje natural, que no
sólo contemple las conexiones “externas” entre los enunciados simples, sino que extienda a la
lógica clásica proposicional en dos direcciones:
permita expresar que, dado un universo del discurso, una cierta propiedad la satisface un
ente concreto, o bien todos los entes, o la satisface algún ente o no la satisface ningún ente
de dicho universo. 1
El marco mı́nimo para dicho propósito lo proporciona la lógica conocida como Lógica de Predi-
cados de Primer Orden o simplemente como la Lógica de Primer Orden, a la que denotaremos
por L1 .
Wilfred Hodges hace la siguiente reflexión:
. . . la lógica de primer orden es hija de varios padres; al menos tres grupos diferentes
de pensadores han tenido que ver en su concepción y con tres motivos muy diferentes:
Los lógicos tradicionales desde Aristóteles hasta George Boole (1815-1864) se-
guidos, entre otros, por Augustus de Morgan (1806-1871) y Charles S. Peirce
(1839-1914). Para ellos el objetivo central fue proporcionar esquemas de razo-
namientos válidos.
Los teóricos de la demostración, entre los que hemos de incluir Gottlob Fre-
ge (1848-1925), Giuseppe Peano (1858-1932), David Hilbert (1862-1943), Ber-
trand Russell (1872-1970), Jacques Herbrand (1908-1931) y Gerhard Gentzen
(1909-1945). Para ellos el objetivo fue sistematizar el razonamiento matemáti-
co de modo que las hipótesis fueran explicitadas y las etapas fueran descritas
rigurosamente.
Los centrados en la teorı́a de modelos, entre los que cabe destacar Ernest Schröder
(1841-1902), Leopold Löwenheim (1878-1957), Thoralf Skolem (1887-1963),
Kurt Gödel (1906-1978) y Alfred Tarski (1909-1945). Para ellos el objetivo fue
estudiar estructuras matemáticas desde el punto de vista de las leyes que dichas
estructuras obedecen.
1
En definitiva, vamos a estudiar una lógica que permite analizar razonamientos en los que las hipótesis y la
conclusión son frases del lenguaje natural del mismo tipo que las contempladas en la lógica proposicional que hemos
estudiado en el primer libro, pero en la que dispondremos de un lenguaje más rico que nos permitirá expresar la
estructura predicativa de dichas frases.
1.1. LENGUAJE L1 DE UNA LÓGICA DE PRIMER ORDEN 3
Quizás esta mezcla es la causa de su fuerza. Sin embargo, sea cual sea la razón, la
lógica de primer orden es la lógica moderna más simple, más potente y más aplica-
ble. . .
representar elementos arbitrarios del dominio o universo del discurso, por medio de sı́mbo-
los de variable.
representar elementos especı́ficos del universo del discurso, por medio de sı́mbolos de
constante.
representar generadores de elementos del universo del discurso a partir de uno o varios
elementos de dicho universo, por medio de sı́mbolos de función.
expresar que nos referimos a algunos o a todos los elementos del universo del discurso, por
medio de sı́mbolos de cuantificación o cuantificadores.
expresar propiedades o relaciones entre los elementos del universo del discurso, por medio
de sı́mbolos de predicado.
1.1.1. Alfabeto
El alfabeto de un lenguaje de primer orden consta de los siguientes sı́mbolos:
aΣ = Σ ∪ V ∪ {¬, ∧, ∨, →, ↔, ∀, ∃, , , (, )}
las primeras letras del alfabeto a, b, c, . . . (posiblemente subindizadas) para representar los
sı́mbolos de constantes.
1.1. LENGUAJE L1 DE UNA LÓGICA DE PRIMER ORDEN 5
las últimas letras del alfabeto x, y, z, . . . (posiblemente subindizadas) para representar los
sı́mbolos de variables.
Términos:
Definición 1.2 Sea a un alfabeto para la lógica de primer orden y a⋆ el conjunto de las cadenas
sobre a, es decir, el lenguaje universal sobre a.
Para cada sı́mbolo f ∈ F de aridad n, definimos la función Cf : (a∗ )n −→ a∗ mediante:
Cf (t1 , . . . , tn ) = f (t1 , . . . , tn )
El conjunto de los términos sobre a es la clausura inductiva del conjunto V ∪ C para el conjunto
de constructores {Cf | f ∈ F}. Denotaremos por Term el conjunto de términos.
Usualmente, el conjunto de los términos se presenta, más informalmente, de la manera siguiente:
Los términos sobre a son los elementos de a∗ determinados por las siguientes reglas:
1. Las variables y los sı́mbolos de constantes son términos.
Definición 1.3 Los términos en los que no ocurren variables se llaman términos básicos.
f (g(a, x)); g(f (x), g(x, y)) y g(a, g(a, g(a, f (b))))
Los predicados se aplican sobre los términos para formar las fórmulas atómicas.
Definición 1.4 Los átomos o fórmulas atómicas son los elementos de a⋆ de la forma
P (t1 , . . . , tn ), donde P es un sı́mbolo de predicado n-ario y t1 , . . . , tn son términos. Denotaremos
por Atom el conjunto de átomos. Los átomos son las fbfs más simples de L1 (de ahı́ el adjetivo
de “atómica”).
Definición 1.5 Los átomos en los que no intervienen variables se llaman átomos básicos y
son las expresiones más sencillas del lenguaje que son interpretables como aserciones (afirmamos
que una n-upla de objetos están en una determinada relación n-aria).
Tenemos ya todo lo necesario para definir el conjunto de fbfs, esto es, el lenguaje. Los cuantifica-
dores y los conectivos permitirán obtener fbfs complejas a partir de los átomos de modo similar
al caso proposicional.
Ux , Ex : a∗ −→ a∗
{C¬ , C∧ , C∨ , C→ , C↔ } ∪ {Ux , Ex | x ∈ V}
De manera menos formal, podemos describir el conjunto de las fbfs, como el conjunto de los
elementos de a∗ determinados por las siguientes reglas:
1. ⊤ y ⊥ son fbfs.
1.1. LENGUAJE L1 DE UNA LÓGICA DE PRIMER ORDEN 7
Notación: En todo lo que sigue usaremos el sı́mbolo Q para representar un sı́mbolo de cuan-
tificación, es decir, un elemento del conjunto {∀, ∃}. Diremos que ∀ y ∃ son sı́mbolos duales de
cuantificación y usaremos Q b para indicar el dual de Q, es decir, b
∀=∃yb ∃ = ∀.
r r Advirtamos que después de un sı́mbolo de cuantificación sólo está permitido un sı́mbolo
ee
de variable y que los argumentos de un sı́mbolo de predicado han de ser términos. Estos
hechos caracterizan a los lenguajes de primer orden, diferenciándolos de los lenguajes de
orden superior. En un lenguaje de primer orden:
sólo se dispone de variables de individuos.
no se puede cuantificar sobre sı́mbolos de función ni sobre sı́mbolos de predicado.
sólo se puede “predicar” sobre individuos.
En un lenguaje de segundo orden, existe un conjunto infinito numerable de sı́mbolos de
variables de predicado y también sı́mbolos de cuantificación universal y existencial sobre
estas variables. Ésto da al lenguaje de segundo orden mayor potencia expresiva; por ejemplo,
la igualdad es definible por la siguiente fórmula debida a Leibnitz
donde, para mayor legibilidad, nos hemos permitido usar el sı́mbolo de predicado binario
“=” con notación infija.
Ejemplo 1.2
1. (∀x)(∀y)(R(x, y) ↔ R(y, x)) es una fbf que expresa que R representa una relación simétri-
ca.
2. (∃x)¬R(x, x) es una fbf que expresa que R representa una relación no reflexiva.
3. (∀x)(∃y)R(x, y) es una fbf que expresa que R representa una relación total.
Ejemplo 1.3
1. El enunciado “Todos los alumnosde esta clase tienen más de 18 años” puede ser expresado
en L1 por: (∀x) C(x) → M (x) , donde C(α) simboliza “α es alumno de esta clase” y
M (α) simboliza “α tiene más de 18 años”.
8 CAPÍTULO 1. LÓGICA DE PRIMER ORDEN
2. El enunciado “No todas las aves pueden volar” puede ser formalizado en L1 por:
¬(∀x) A(x) → V (x)
3. El enunciado “Hay alumnos de esta clase que tienen más de 24 años” puede ser formalizado
en L1 por: (∃x) C(x) ∧ E(x) , donde C(α) simboliza “α es alumno de esta clase” y E(α)
simboliza “α tiene más de 24 años”.
4. El razonamiento:
I(a)
5. El razonamiento:
I(s(a))
6. El razonamiento:
Hay quien, aun siendo coherente, sólo se preocupa de sus propios problemas.
Todo el mundo se preocupa por las cuestiones del medio ambiente, a menos que sea
un irresponsable.
Toda persona coherente es responsable.
1.1. LENGUAJE L1 DE UNA LÓGICA DE PRIMER ORDEN 9
Por lo tanto, hay quien es coherente y toma como propio el problema del medio
ambiente 2 .
donde C(α) formaliza “α es coherente”, Q(α, β) formaliza “α se preocupa por β”, P (α, β)
formaliza “α es un problema para β”, R(α) formaliza “α es responsable y a formaliza
“Cuestiones del medio ambiente”.
lenguaje de la lógica de primer orden como clausuras inductivas, podemos, tal como explicamos
en el libro de lógica proposicional, utilizar el principio de inducción estructural para verificar
propiedades sobre tales conjuntos:
Todos los términos de L1 (Σ) tienen la propiedad P con tal de que se cumpla:
Todas las fbfs de L1 (Σ) tienen la propiedad P con tal de que se cumpla:
El grado de una fbf consiste en el número de operadores lógicos que intervienen en ella:
Definición 1.8 Denotemos el grado de una fbf A mediante gr(A). Entonces definimos:
1. gr(A) = 0, si A es un átomo
2. gr(¬A) = 1 + gr(A)
4. gr((Qx)A) = 1 + gr(A)
Todos los términos de L1 (Σ) tienen la propiedad P con tal de que se cumpla:
Todas las fbfs de L1 (Σ) tienen la propiedad P con tal de que se cumpla:
1.1. LENGUAJE L1 DE UNA LÓGICA DE PRIMER ORDEN 11
Una vez definido qué entendemos por un lenguaje de primer orden estamos interesados, como
en el caso proposicional, en introducir la noción de subfórmula de una fbf.
Definición 1.9 En esta definición usaremos de nuevo el sı́mbolo “∗” para representar un
conectivo booleano binario arbitrario, es decir, un elemento del conjunto {∨, ∧, →, ↔}.
La función subfórmula, que asigna a cada fbf A el conjunto de todas sus subfórmulas, sub(A),
se define recursivamente como sigue:
Ejemplo
1.4
sub (∃x)(R(x) → (∀y)¬T (x, y) ) =
{((∃x)(R(x) → (∀y)¬T (x, y)), R(x) → (∀y)¬T (x, y), R(x), (∀y)¬T (x, y), ¬T (x, y), T (x, y)}
1. TA es A, si A es un átomo
¬
2. T¬A es TA
∗
@
@
3. TA∗B (donde ∗ ∈ {∧, ∨, →, ↔}) es TA TB
Qx
4. TQxA es TA
es
∧
H
HH
∃x ¬
→ ∃z
@
@
R(x) ∀y →
@
@
¬ ∀u ∀v
Como en el caso proposicional, las subfórmulas de una fbf quedan caracterizadas en términos de
los subárboles del árbol sintáctico de la fbf:
B es una subfórmula de A si y sólo si TB es un subárbol de TA .
1. R(x) → (∀y)T (x, y) , (∀y)¬T (x, y) y ¬(∃z)((∀u)P (u, z) → (∀v)Q(v, z)) ocurren positiva-
mente en A.
1.1.4.1. Notación
Usaremos las mismas notaciones que en la lógica proposicional: A[B] denota que B es una
subfórmula de A y A[B/C] denota que al menos una ocurrencia de B en A se ha sustituido por
la fbf C.
→
H
HH
∀x ∃y
P (x, z) ∧
@
@
Q(z) R(y, z)
r r Nótese que, dada una fbf, A, una misma variable, x, puede ser libre y ligada a la vez en A.
ee
Ejemplo 1.8
1. En la fbf
((∀x)P (x, y, a) ∨ Q(b, f (x, c)) → (∃y)(Q(d, y) ∧ D(y))
las dos primeras ocurrencias de x son ligadas y la tercera libre, mientras que la variable y
es libre en la primera ocurrencia y ligada en las tres restantes.
2. En la fbf
(∀x)P (x, y) → (∃y)(P (x, y) ∧ Q(z))
las dos primeras ocurrencias de x son ligadas mientras que la tercera es libre. La primera
ocurrencia de la variable y es libre, el resto, son ocurrencias ligadas. La única aparición de
la variable z es libre.
Podemos definir el conjunto de las variables libres y de las variables ligadas de una fbf recursi-
vamente como sigue:
Definición 1.14 El conjunto de variables libres de una fbf A, denotado Vlibre (A) se define
recursivamente como sigue:
1. Vlibre (P (t1 , . . . , tn )) = V(t1 ) ∪ · · · ∪ V(tn ), donde V(ti ) denota el conjunto de variables que
intervienen en el término ti .
Definición 1.15 El conjunto de variables ligadas de una fbf A, que denotaremos Vligada (A),
se define recursivamente como sigue:
3
La noción de variable libre en una fbf es fundamental para trabajar en los lenguajes de primer orden. Intui-
tivamente, las variables libres son aquellas que pueden ser sustituidas.
1.1. LENGUAJE L1 DE UNA LÓGICA DE PRIMER ORDEN 15
1. Vligada (P (t1 , . . . , tn )) = ∅.
2. Vligada (¬A) = Vligada (A).
3. Vligada (A ∗ B) = Vligada (A) ∪ Vligada (B), donde ∗ ∈ {∧, ∨, →, ↔}.
4. Vligada ((Qx)A) = Vligada (A) ∪ {x}.
Como hemos indicado, para una fbf A, la intersección de Vlibre (A) y Vligada (A) no necesariamente
es el conjunto vacı́o. Ası́, para la fbf
A = ((∀x) P (x, a, z) ∨ Q(b, f (x, c)) → (∃y)(C(d, y) ∧ D(y))
se tiene que Vlibre (A) = {x, z} y Vligada (A) = {x, y}.
Notación: Para expresar que las variables x1 , . . . , xn son libres en la fbf A escribiremos
A(x1 , . . . , xn ). Con esta notación destacamos que {x1 , . . . , xn } es un subconjunto de Vlibre (A),
pero téngase en cuenta que este subconjunto puede ser propio, es decir, la notación A(x1 , . . . , xn )
no exige que x1 , . . . , xn sean las únicas variables con ocurrencias libres en A, son simplemente
variables que queremos destacar.
Definición 1.16 Una fbf A es cerrada o un enunciado si Vlibre (A) = ∅.
Definición 1.17 Si Vlibre (A) = {x1 , . . . , xn }, se llama cierre universal de A a la fbf
(∀x1 )(∀x2 ) . . . (∀xn )A(x1 , . . . , xn )
Se llama cierre existencial de A a la fbf
(∃x1 )(∃x2 ) . . . (∃x1 )A(x1 , . . . , xn )
Las variables son sı́mbolos que representan a elementos arbitrarios del universo de discurso.
En el desarrollo de algoritmos, transformaciones,etc, necesitaremos “particularizar” las fbfs a
elementos concretos o menos arbitrarios; esto lo haremos mediante la sustitución de variables:
r r Es obvio que el proceso de renombramiento en una fbf, A, tan sólo modifica Vligada (A). El
ee
conjunto de las variables libres, Vlibre (A), no se modifica. Ası́, en el ejemplo anterior,
Notación:
1. Sea x una variable y sea t1 , t2 términos. Denotaremos mediante [x/t2 ]t1 el término resul-
tante de sustituir en t1 las apariciones de la variable x por el término t2 .
2. Sea x ∈ Vlibres (A). La fbf que se obtiene a partir de la fbf A por sustitución de todas
las ocurrencias libres de la variable x por un término t, la denotaremos por [x/t]A. Si
representamos la fbf A por A(x) para destacar que x tiene ocurrencias libres en A, usaremos
la expresión A(t) para representar a [x/t]A.
Inductivamente:
Definición 1.19
Definición 1.21 Dada la fbf A(x) y el término básico (sin variables), t, a la fbf [x/t]A(x) la
denominamos una instancia básica de A(x). El mecanismo de sustituir una variable ligada
por un término básico se denomina “instanciación”. 4
4
Somos conscientes de que esta denominación es desafortunada, quizás deberı́amos haber optado por “concre-
ción” en lugar de “instanciación”. La decisión final ha venido condicionada por el uso habitual que se hace de
esta expresión.
1.1. LENGUAJE L1 DE UNA LÓGICA DE PRIMER ORDEN 17
En la práctica, desearemos obtener una fbf B a partir de otra fbf A mediante la sustitución en
A de variables por términos y de modo que el significado de A y B sea el mismono. Aún no
hemos descrito la semántica para los lenguajes de primer orden, pero aún ası́, no dudamos en
afirmar que si sustituimos en la fbf
en la que existe una interacción entre el cuantificador (∀x) y su rango, que no existı́a en A. Por
lo tanto, si deseamos no alterar es significado de las fbfs, el mecanismo general para sustituir
una variable por un término, requiere ciertas precauciones que nos aseguren que sustituimos
ocurrencias libres en A por “términos libres” en A. En definitiva, como tendremos ocasión de
comprobar cuando estudiemos la semántica, para evitar este hecho conocido en la bibliografı́a
como conflicto de variables,5 requerimos la siguiente definición:
Definición 1.22 Sea A una fbf, x ∈ Vlibre (A) y t un término en el que intervienen las variables
V(t) = {x1 , . . . , xn }. Se dice que el término t es libre para x en A(x) (o bien que x es
sustituible por t en A(x)) si, para toda variable xi ∈ V(t), se tiene que ninguna ocurrencia
libre de x en A está en el rango de una ocurrencia en A del cuantificador (Qxi ). Es decir, las
ocurrencias de xi surgidas como consecuencia de la sustitución de x por t, son ocurrencias libres
en A(t).
Ejemplo 1.10
3. En la fbf (∀y)P (x, y) → (∃x)Q(x, z, a), el término f (a, y) no es libre para x, pero sı́ es
libre para z.
5
Variable clash en la bibliografı́a inglesa.
18 CAPÍTULO 1. LÓGICA DE PRIMER ORDEN
La siguiente definición, establece cómo obtener [x/t]A, diferenciando los casos en que el término
t es o no libre para la variable x en A(x).
Definición 1.23 Si t es libre para x en A(x), la sustitución en A de x por t consiste en sustituir
en A las ocurrencias libres de x por t.
Si t no es libre para x en A(x) y V(t) = {x1 , . . . , xn }, la sustitución en A de x por t consiste en
1. Renombrar en A las variables xi tales que x ocurre en el rango de (Qxi ) por una variable
de renombramiento que no ocurra en t.
El término f (a, y, z) no es libre para x. Para realizar la sustitución de x por el término f (a, y, z)
podemos proceder como sigue:
1. Como x ocurre libre en el rango de (∀z) y (∃y), renombramos la variable y y la variable
z, por ejemplo, por v y u respectivamente (que no ocurren en f (a, y, z)), obteniendo
2. En segundo lugar, sustituimos las ocurrencias libres de x en A por f (a, y, z). Obtenemos
ası́ la fbf:
(∀u)(P (f (a, y, z)) → (∃x)Q(x, u)) ∨ (∃v)D(f (a, y, z), v)
r r Las variables tienen en lógica un papel análogo al que tienen en análisis o en álgebra. Veamos
ee
algunos ejemplos:
− En la función descrita por f (x) = x + 6, la variable x no designa un objeto, sino el
emplazamiento de un objeto, el lugar del cuerpo de la función en el que ha de colocarse un
argumento para evaluar la función. La variable x está ligada; más precisamente, la primera
ocurrencia de x crea una ligadura, a la que se enganchan las demás ocurrencias de x. No hay
inconveniente alguno en renombrar x, es decir, reemplazar las dos ocurrencias de x por y:
f (y) = y + 6. Pero obviamente, no está permitido reemplazar una ocurrencia solamente:
f (x) = y + 6; f (y) = x + 6
Sk=8
− En la expresión k=1 Aki , la variable i es una variable libre y k es una variable ligada.
Se puede por lo tanto renombrar k, por ejemplo, por j sin alterar su significado, pero no
podemos renombrar k por i.
− Si consideramos la fórmula para evaluar una integral doble según el teorema de Fubini
Z Z !
b h(y)
f (x, y)dx dy.
a g(y)
en la expresión entre paréntesis todas las ocurrencias de x están ligadas (por la ligadura dx),
sin embargo las de y son ocurrencias libres, en el sentido de que no han de ser evaluadas en
la primera etapa.
1.2. SEMÁNTICA PARA LOS LENGUAJES DE PRIMER ORDEN 19
en ella existe un cuantificador (Qx) en el rango de un cuantificador (Q′ x), es decir, existe un
anidamiento de cuantificadores con la misma variable de cuantificación. Es posible (y deseable,
como posteriormente nos confirmará la semántica) evitar la situación anterior restringiendo la
regla que permite construir fbfs cuantificadas del siguiente modo:
Definición 1.24 Si x es una variable y A es una fbf sin ocurrencias ligadas de x entonces
(∀x)A y (∃x)A son fbfs.
Por otra parte, si la fbf contiene variables libres, debemos especificar qué valores del dominio
representan. Ası́, dada la fbf (∀x)P (x), si consideramos U = N y asignamos a P el significado
20 CAPÍTULO 1. LÓGICA DE PRIMER ORDEN
“es par”, podemos asegurar que la fbf es falsa en esta interpretación. Pero nada podemos afirmar
sobre la fbf P (x) si no nos pronunciamos sobre el número natural representado por x. Análo-
gamente, podemos pensar en una interpretación en la que la fórmula 2 + 3 = 5 es verdadera,6
pero no podremos pronunciarnos sobre la verdad o no de la fórmula x + 3 = 4 si no sabemos el
número representado por x.
Ocurre como en un procedimiento con parámetros en un programa PASCAL, el procedimiento
no puede computarse salvo que sea llamado con parámetros actuales, por ejemplo P (10, 35).
Deseamos, pues, disponer de un concepto de interpretación que nos permita:
asignar a toda fbf cerrada o enunciado (sin variables libres) el valor de verdad 0 ó 1,
contemplar una fbf con variables libres como una afirmación sobre el dominio, que es
verdadera o falsa dependiendo de la asignación realizada a las variables libres.
ξ : V −→ U
Definición 1.27 Dada una interpretación (U, I) y una valuación de variables ξ asociada a
ella, definimos recursivamente una aplicación Iξ , llamada función de significado, que asigna
a cada término t un elemento Iξ (t) ∈ U como sigue:
r r Obsérvese que si un término t es básico (sin variables), el significado en U asignado por una
ee
función de significado Iξ a t no depende del entorno ξ. Ası́, por ejemplo, si g es un sı́mbolo
de función monaria y a es un sı́mbolo de constante, Iξ (f (a)) = I(f )(I(a)). En adelante, por
abuso de notación, si t es un término básico escribiremos I(t) en lugar de Iξ (t). Ası́ pues,
escribiremos I(f (a)) en lugar de Iξ (f (a)).
Ahora, nuestro objetivo es introducir las nociones de satisfacibilidad y de validez. Para ello
requerimos previamente conocer el valor de verdad asignado por una función de valuación a una
fbf.
Definición 1.28 Dada una interpretación (U, I) y una valuación de variables ξ asociada a
(U, I), definimos el valor de verdad de un átomo como sigue: Iξ (⊥) = 0, Iξ (⊤) = 1 y
La definición para las fbfs (∀x)A y (∃x)A requiere una definición previa que permite expresar
la asignación de valores a una variable concreta.
Definición 1.29 Dos valuaciones de variables ξ y ξ ′ se dicen x-equivalentes si ξ ′ (y) = ξ(y)
para toda variable y 6= x.
Obviamente, dado un sı́mbolo de variable x, la relación de x-equivalencia es una relación de
equivalencia en el conjunto de valuaciones de variables.
Definición 1.30
2. Una fbf A se dice verdadera en una interpretación (U, I), denotado |=(U,I) A o bien por
I(A) = 1 (si no hay lugar a confusión), si para toda valuación de variables ξ se tiene que
Iξ (A) = 1.
1.2. SEMÁNTICA PARA LOS LENGUAJES DE PRIMER ORDEN 23
4. Una fbf A se dice insatisfacible o que es una contradicción, si Iξ (A) = 0 para toda
interpretación (U, I) y toda valuación de variables ξ.
r r El siguiente ejemplo nos advierte de un posible error, confundir los conceptos de fbf verdadera
ee
en una interpretación, I, y fbf satisfacible:
- Para que una fbf A sea verdadera en una interpretación, I, se requiere que para toda
valuación ξ se tenga que Iξ (A) = 1.
- Para que una interpretación, I, satisfaga o modelize a una fbf, A, basta que para alguna
valuación ξ se tenga que Iξ (A) = 1.
Definición 1.32 Una interpretación para un conjunto finito de fbfs, Ω (en particular
para una fbf A) es una tupla de la forma
donde ui son los elementos de U asignados a los sı́mbolos de constantes {a1 , . . . an } que inter-
vienen en Ω, Fi son las funciones sobre U asignadas a los sı́mbolos de funciones {f1 , . . . fm } que
intervienen en Ω y Ri son las relaciones en U asignadas a los sı́mbolos de predicado {P1 , . . . Pk }
que intervienen en Ω.
Ejemplo 1.12 Una interpretación para (∀x)(P (x) → Q(f (x), a)) es
({1, 2, 3}; {a ; 1}; {f ; {(1, 2), (2, 1), (3, 3)}}; {P ; {2}, Q ; {(1, 1), (1, 2)}}) 8
Definición 1.33 Una estructura para una fbf A es una tupla de la forma
donde
8
En definitiva, una interpretación M para un conjunto finito de fbfs Ω, es la restricción de una interpretación
(U, I) al conjunto de sı́mbolos de constantes, de sı́mbolos de funciones y de sı́mbolos de predicado que intervienen
en Ω. En adelante, para expresar el valor de verdad asignado por M a A seguiremos escribiendo I(A).
24 CAPÍTULO 1. LÓGICA DE PRIMER ORDEN
Definición 1.34 Una estructura para un conjunto finito de fbfs Ω es una tupla de la
forma
(CΩ , FΩ , PΩ ; U ; {d1 , . . . , dn }; {F1 , . . . , Fm }; {R1 , . . . , Rk })
donde
Ejemplo 1.13
1. Veamos que P (x, 0) es satisfacible. En efecto, sea la interpretación (Z, I) con I(P ) = “ ≤′′ .
Para toda valuación de variables, ξ, tal que ξ(x) ≤ 0 se tiene que Iξ (P (x, 0)) = 1. Sin
embargo, P (x, 0) no es verdadera en (Z, I), ya que para toda valuación, ξ, tal que ξ(x) > 0
se tiene que Iξ (P (x, 0)) = 0.
Puesto que en la fbf sólo interviene el sı́mbolo de variable x, dada una valuación de va-
riables, estamos únicamente interesados en qué valor asigna ésta a x, es decir, en las
valuaciones de variables ξ tales que ξ(x) = 1 y en las valuaciones de variables ξ ′ tales que
ξ ′ (x) = 2. Obviamente, cada valuación x-equivalente a una del primer tipo es del segundo
tipo y viceversa.
Para estas valuaciones se tiene que:
ee
r rLas valuaciones de tipo ξ1 y de tipo ξ4 son x-equivalentes.
Las valuaciones de tipo ξ2 y de tipo ξ3 son x-equivalentes.
Las valuaciones de tipo ξ1 y de tipo ξ3 son y-equivalentes.
Las valuaciones de tipo ξ2 y de tipo ξ4 son y-equivalentes.
Los siguientes resultados son de gran interés para poder facilitar la manipulación semántica de
las fbfs.
Teorema 1.2 Sea una fbf A y sea M = (U, I) una interpretación de L1 , entonces si ξ y ξ ′ son
dos valuaciones de variables tales que ξ(x) = ξ ′ (x) para toda variable x tal que x ∈ Vlibre (A), se
tiene que
Iξ (A) = 1 si y sólo si Iξ ′ (A) = 1
Iξ (A) = 1 si y sólo si Iξ (B) = Iξ (C) = 1 y, puesto que Vlibre (A) = Vlibre (B) ∪
Vlibre (C), por la hipótesis de inducción tenemos que, Iξ ′ (B) = Iξ (B) y Iξ ′ (C) =
Iξ (C).
• y ∈ Vlibre (B).
Entonces µ(y) = µ′ (y) (por def. de µ), luego µ(y) = ξ ′ (y). Ahora bien, por hipótesis,
ξ y ξ ′ coinciden en los valores asignados a las variables de Vlibre (B), por tanto, µ(y) =
ξ(y).
• y∈
/ Vlibre (B).
Entonces µ(y) = ξ ′ (y) (por def. de µ) y obtenemos el mismo resultado que antes.
A partir de lo anterior resulta, entonces, que Iµ (B) = 1, pues Iξ (A) = 1. Ahora bien puesto
que µ(y) = µ′ (y) para toda y ∈ Vlibre (A), por hipótesis de inducción, Iµ′ (B) = Iµ (B) y
entonces Iµ′ (B) = 1. Por tanto, se tiene que Iξ ′ (A) = 1.
La demostración del inverso es análoga.
Teorema 1.3 Dada una fbf cerrada A y una interpretación M = (U, I), se tiene que I(A) = 1
o bien I(A) = 0
Demostración: Puesto que A no tiene variables libres, dos valuaciones de variables cuales-
quiera ξ y ξ ′ cumplen la hipótesis del teorema anterior. Por lo tanto, Iξ (A) = 1 si y sólo si
Iξ ′ (A) = 1. Ası́ pues, Iξ (A) = 1 para toda valuación de variables ξ o bien Iξ (A) = 0 para toda
valuación de variables ξ, es decir, I(A) = 1 ó I(A) = 0.
1.2. SEMÁNTICA PARA LOS LENGUAJES DE PRIMER ORDEN 27
Demostración:
1. Es evidente.
Una vez demostrado el Teorema 1.4 podemos plantearnos redefinir la semántica limitándonos a
la consideración de las fbfs cerradas:
Definición 1.35 Si t1 , . . . , tn son términos básicos y
Esta definición se extiende recursivamente a todas las fbfs cerradas del siguiente modo:
Si M = (U ; {u1 , . . . un }; {F1 , . . . Fm }; {R1 , . . . Rk }) es una interpretación para el conjunto de fbfs
cerradas {A, B}, entonces, I(⊥) = 0; I(⊤) = 1 y:
1. I(¬A) = 1 si y sólo si I(A) = 0
Iu0 ([x/b]B) = 1
Iu0 ([x/b]B) = 1
Los ejemplos expuestos hasta aquı́ nos muestran que, a diferencia de la lógica clásica proposi-
cional, en la lógica clásica de primer orden, es laborioso analizar la satisfacibilidad o la validez
de una fbf. Incluso en ejemplos tan sencillos como los que hemos considerado, nos sentimos
agobiados por los formalismos. Pero no son los formalismos el único handicap, más adelante
probaremos que los problemas de la satisfacibilidad y la validez no son decidibles en L1 : son tan
sólo semidecidibles, ¡es el precio a pagar por su mayor expresividad!
Por ahora, nos conformaremos con analizar fbfs sencillas haciendo uso de la definición. Pero
incluso para este análisis, en los ejemplos siguientes, nos vamos a permitir expresarnos menos
formalmente.
Ejemplo 1.14 Consideremos el conjunto de fbfs
(a) En la interpretación
({a, b, c}; {a ; a}; ∅; {P ; {a, b}, Q ; {(a, b), (a, c), (b, a), (c, a)}})
P (a) es, obviamente, verdadera. Veamos que (∀x)(∃y)(P (x) → Q(y, x)) también lo es.
Informalmente, podemos razonar como sigue:
(b) En la interpretación
P (a) es, obviamente, verdadera. Veamos que (∀x)(∃y)(P (x) → Q(y, x)) no lo es:
Si asignamos 8 a x, para cualquier asignación de un número entero m a y, se tiene que
8 6= m2 y, por lo tanto, (∀x)(∃y)(P (x) → Q(y, x)) no es verdadera.
(c) En la interpretación
P (a) es, obviamente, falsa. Veamos que (∀x)(∃y)(P (x) → Q(y, x)) es verdadera:
Debido a que la semántica de los conectivos booleanos es la misma que para la lógica proposi-
cional, la noción de tautologı́a es extensible a la lógica de primer orden: Es inmediato que
(A → B) ↔ (¬A ∨ B)
Para probar que una fbf, A, en L1 no es válida, se requiere encontrar una interpretación en la
que dicha fbf sea falsa, es decir, un contramodelo para A.
Ejemplo 1.16 La fbf (∀x)(∃y)P (x, y) → (∃y)(∀x)P (x, y) no es válida ya que la interpretación
(N; ∅; ∅; {P ;≤}) es un contramodelo, es decir, un modelo para su negación.
Definición 1.38 Dos fbfs A y B se dice que son lógicamente equivalentes, denotado A ≡ B,
si A ≡M B para toda interpretación M en L1 . Obviamente,
A ≡M B si y sólo si A ↔ B es verdadera en M
A ≡ B si y sólo si A ↔ B es válida
(∀x)A ≡ ¬(∃x)¬A
(∃x)A ≡ ¬(∀x)¬A
O ∪ {∀} y O ∪ {∃}
{∧, ¬, ∀} y {¬, →, ∃}
r r Conviene hacer de nuevo hincapié en que una frase del lenguaje natural (de las contem-
ee
pladas por la lógica clásica de primer orden), como ocurrı́a en el caso proposicional, puede
ser formalizada por diversas fbfs del lenguaje L1 (más aún, por una infinidad numerable
de fbfs) todas ellas semánticamente equivalentes, es decir, que transmiten la misma infor-
mación. Ası́ pues, “No todas las aves pueden volar” puede ser puede ser formalizada por
¬(∀x) A(x) → V (x) , donde A(α) formaliza
“α es un ave” y V (α) formaliza “α puede
volar”, o bien por (∃x) A(x) ∧ ¬V (x) , es decir “Existen aves que no pueden volar”.
Por lo tanto, ante una frase del lenguaje natural, nuestro quehacer habrá de centrarse en re-
flexionar cuál es la información que deseamos transmitir para después proceder a formalizarla
mediante L1 .
Demostración de 5:
El resto de las demostraciones son similares.
Supongamos que x no ocurre en B. 10 Sea (U, I) una interpretación cualquiera de L1 tal que
Iξ ((∀x)(A(x) ∨ B)) = 0. Entonces existe una valuación de variables ξ ′ x-equivalente a ξ tal que
Iξ ′ (A(x) ∨ B) = 0; es decir, Iξ ′ (A(x)) = Iξ ′ (B) = 0. Es claro, entonces, que Iξ ((∀x)A(x)) = 0.
Además, dado que x no ocurre en B, entonces ξ y ξ ′ asignan exactamente los mismos valores a
todas las variables de Varlibre (B), luego –por el Teorema 1.2– tenemos también que Iξ (B) = 0.
Por consiguiente, Iξ ((∀x)A(x)∨B) = 0. La recı́proca se demuestra de forma similar. Esto prueba
que para cualquier interpretación y valuación de variables asociadas a dicha interpretación ambas
fórmulas reciben el mismo valor de verdad. Por tanto, ambas son equivalentes.
10
Se podrı́a admitir que x no ocurriera libre en B.
32 CAPÍTULO 1. LÓGICA DE PRIMER ORDEN
Demostración: Sea M = (U, I). Si B ≡M C, por definición de ≡M , se tiene que, para toda
valuación ξ, Iξ (B) = Iξ (C).
Tenemos que probar que Iξ (A) = Iξ (A[B/C]) para toda valuación ξ. Lo demostramos por
inducción estructural:
Como corolario de este teorema, se tiene el siguiente resultado que generaliza el teorema del
mismo nombre para la lógica clásica proposicional.
Lema 1.1 Dada una fbf A y z un sı́mbolo de variable que no ocurre en A(x), entonces:
1. (Qz)A ≡ A
2. (Qx)A(x) ≡ (Qz)A(z)
1. Los átomos junto con sus negaciones se llaman literales. Decimos que los literales P (t1 , . . . , tn )
y ¬P (t1 , . . . , tn ) son literales opuestos.
2. Una fbf se dice que es un cubo si es ⊤, ⊥ o una conjunción finita (posiblemente vacı́a)
de literales.
3. Una fbf se dice que es una cláusula si es ⊤, ⊥ o una disyunción finita (posiblemente
vacı́a) de literales.
4. Una fbf en la que los únicos conectivos booleanos que intervienen son ¬, ∧ y ∨ y en la que
¬ sólo afecta a los átomos se dice que es una forma normal negativa, denotada fnn.
Definición 1.40
1. Una fbf se dice que es una forma normal prenexa, denotada fnp, si es de la forma
(Q1 x1 ) . . . (Qn xn )B donde
Dada una fnp, A = (Q1 x1 ) . . . (Qn xn )B, a la secuencia (Q1 x1 ) . . . (Qn xn ) se le denomina
prefijo de A y a la fbf B se le denomina matriz de A.
2. Una fbf se dice que es una forma normal prenexa disyuntiva, denotada fnpd, si es
⊤, ⊥, o una forma normal prenexa en la que su matriz es una disyunción de cubos.
3. Una fbf se dice que es una forma normal prenexa conjuntiva, denotada fnpc, si es
⊤, ⊥, o una forma normal prenexa en la que su matriz es una conjunción de cláusulas.
Las nociones de cláusula que contiene a otra cláusula y cubo que contiene a otro cubo son las
mismas que para el caso proposicional. Asimismo, se generalizan de modo natural los conceptos
de forma normal conjuntiva restringida y forma normal disyuntiva restringida:
Definición 1.41 Una fnpd se dice restringida, denotada fnpdr, si su matriz cumple los
siguientes requisitos:
Una fnpc se dice restringida, denotada fnpcr, si su matriz cumple los siguientes requisitos:
Teorema 1.9 Para toda fbf de L1 existe una forma normal prenexa disyuntiva restringida y
una forma normal prenexa conjuntiva restringida equivalentes a ella.
Paso 1: Hacer uso del Corolario 1.1 y realizar cuantos renombramientos sean necesarios para
que en A todas las variables cuantificadas sean distintas.
A ↔ B ≡ (A → B) ∧ (B → A)
A → B ≡ ¬A ∨ B
Paso 3: Usar la ley de doble negación (¬¬A ≡ A), las leyes de Morgan (¬(A ∧ B) ≡ ¬A ∨ ¬B
y ¬(A ∨ B) ≡ ¬A ∧ ¬B) y las leyes
¬(∀x)A ≡ (∃x)¬A
¬(∃x)A ≡ (∀x)¬A
Con los pasos 2 y 3 obtenemos una fbf en la que no interviene → y en la que ¬ afecta
únicamente a los átomos, es decir, obtenemos una fnn.
(∀x)A ∨ B ≡ (∀x)(A ∨ B)
(∀x)A ∧ B ≡ (∀x)(A ∧ B)
(∃x)A ∨ B ≡ (∃x)(A ∨ B)
(∃x)A ∧ B ≡ (∃x)(A ∧ B)
Paso 5: Usar la ley distributiva de ∧ respecto a ∨ (para las fnpdr) o de ∨ respecto a ∧ (para
las fnpcr).
Paso 6: Usar cuantas veces sea posible las leyes (para ∧, o para ∨) de idempotencia, de com-
plementación, de cero y uno y de absorción, para obtener las formas normales restringidas.
Los siguientes ejemplos muestran cómo obtener una fnpcr y una fnpdr equivalente a una fbf
dada.
Ejemplo 1.17 Sea (∃x)[R(x) → ¬(∃y)T (x, y)] ∧ ¬(∃z) [(∀u)P (u, z) → (∀v)Q(v, z)]. Hallemos
una fnpcr y una fnpdr equivalentes a ella:
Ejemplo 1.18 Sea (∀x) P (x) → (Q(x) ∨ ¬R(x)) ∧ (∃y)Q(y). Hallemos una fnpcr y una fnpdr
equivalentes a ella.
(∀x) P (x) → (Q(x) ∨ ¬R(x)) ∧ (∃y)Q(y) ≡
≡ (∀x) ¬P (x) ∨ Q(x) ∨ ¬R(x) ∧ (∃y)Q(y)
≡ (∀x)(∃y) (¬P (x) ∨ Q(x) ∨ ¬R(x)) ∧ Q(y) (fnpc)
≡ (∀x)(∃y) ¬P (x) ∧ Q(y)) ∨ (Q(x) ∧ Q(y)) ∨ (¬R(x) ∧ Q(y)) (fnpd)
1.4. Skolemización
Las formas normales prenexas permiten utilizar los cuantificadores de un modo limitado (solo
en la cabecera de la fbf) sin pérdida de potencia expresiva. Sin embargo, es posible imponer un
uso aún más restringido de la cuantificación que, si bien reduce la potencia expresiva, lo hace
de forma satisfactoria. Concretamente, es posible asociar a toda fbf, A, una fbf, denotada SkA ,
36 CAPÍTULO 1. LÓGICA DE PRIMER ORDEN
llamada forma de Skolem asociada a A que es una forma normal prenexa y en cuyo prefijo
sólo existen cuantificadores universales y tal que A y SkA son equisatisfacibles.
Como conocemos por el estudio de la lógica proposicional, esta pérdida de potencia expresiva
no es demasiado grave, más aún, carece de importancia si estamos interesados en sistemas de
demostración (automática o no) por refutación.
En esta sección, presentamos las formas de Skolem y el proceso a seguir para, dada una fbf A,
obtener SkA . Comencemos analizando algunos ejemplos:
Ejemplo 1.19 Si P es un sı́mbolo de predicado binario, dada la fbf:
(∃x)(∀y)P (x, y)
M = (U ; ∅; ∅; {P ; R})
tal que I( (∃x)(∀y)P (x, y) ) = 1, es decir, si y sólo si, para algún u0 ∈ U , se tiene que Iu0 ((∀y)P (a, y)) =
1, donde a es un sı́mbolo de constante y Iu0 es la interpretación correspondiente a la extensión
de M que asocia u0 al sı́mbolo de constante a, es decir,
Mu0 = (U ; {a ; d0 }; ∅; {P ; R})
Como consecuencia inmediata del resultado del ejemplo anterior, se tiene que:
r r Hasta aquı́, no hemos hecho más que reflejar una práctica habitual en matemáticas: Después
ee
de afirmar la existencia de objetos x que satisfacen una propiedad P (x), continuamos con la
expresión “ sea a alguno de estos x tal que P (a) es cierto”.
¿Podemos eliminar todos los cuantificadores existenciales de esta forma tan sencilla? La respues-
ta, como nos muestra el ejemplo siguiente, es negativa.
1.4. SKOLEMIZACIÓN 37
Ejemplo 1.20
M = {{1, 2}; ∅; {f ; {(1, 2), (2, 1)}}; {P ; {(1, 2), (2, 1)}}}
satisface Ω.
M1 = {{1, 2}; {a ; 1}; {f ; {(1, 2), (2, 1)}}; {P ; {(1, 2), (2, 1)}}}
M2 = {{1, 2}; {a ; 2}; {f ; {(1, 2), (2, 1)}}; {P ; {(1, 2), (2, 1)}}}
y ninguna de ellos satisface Ω′ .
1. Obtener por el procedimiento introducido en la sección anterior una forma normal prenexa,
A′ , equivalente a A.
A continuación presentamos dos ejemplos de fbfs A a las que se asocia una forma normal de
Skolem SkA .
Ejemplo 1.21 Consideremos la fbf
A = (∃y)(∀x)(∀z)(∀u)(∃t) (P (x, y) → Q(a, z, u)) ∧ (P (x, u) → R(t, z))
finalmente, la eliminación de (∃y) y de (∃x) mediante dos etapas de skolemización nos hace
incluir dos sı́mbolos de constante a y b resultando la fbf
(∀z) (P (a) ∧ ¬Q(a)) ∨ ¬P (b) ∨ Q(z)
1.4. SKOLEMIZACIÓN 39
r r Advirtamos que, como avanzamos en la sección anterior, el orden de extracción de los cuan-
ee
tificadores al obtener una forma prenexa equivalente a la fbf dada, influye en la complejidad
de la forma normal de Skolem obtenida. En efecto, puesto que no hemos establecido el orden
de extracción de los cuantificadores, en el ejemplo anterior, podrı́amos haber obtenido la
siguiente forma prenexa
(∀z)(∃x)(∃y) (P (x) ∧ ¬Q(x)) ∨ ¬P (y) ∨ Q(z)
La forma de Skolem asociada es ahora mucho más compleja, puesto que requiere introducir
dos sı́mbolos de función monaria, por ejemplo f y g, obteniendo la fbf
(∀z) (P (f (z)) ∧ ¬Q(f (z))) ∨ ¬P (g(z)) ∨ Q(z)
Es importante, pues, añadir al método para obtener una fnp equivalente a una fbf dada, que la
extracción de los cuantificadores se realiza dando prioridad a los cuantificadores existenciales.
a ⊂ a′
Demostración: Basta probar el resultado para cada una de las etapas de skolemización.
Sea A = (∃x1 ) . . . (∃xn )(∃y)B(x1 , . . . , xn , y) y a un sı́mbolo de constante que no in-
terviene en A. Por la conmutatividad de los cuantificadores existenciales se tiene que
A ≡ (∃y)(∃x1 ) . . . (∃xn )B(x1 , . . . , xn , y). Por lo tanto, basta demostrarlo para una fbf del
tipo A = (∃x)B(x).
Si M = (U, I) es una interpretación en L1 y ξ es una valuación de variables tal que
Iξ ( (∃y)B(y) ) = 1, entonces existe una valuación de variables ξ ′ que es y-equivalente a ξ y
tal que Iξ ′ (B(y)) = 1.
Ahora, si ξ ′ (y) = u, definimos M′ = (U, I ′ ) tal que I ′ difiere de I únicamente en la
interpretación de a y tal que I ′ (a) = u. Entonces, Iξ ′ (B[y/a]) = 1 y, en consecuencia,
B[y/a] es satisfacible.
La demostración del inverso es similar y se deja al lector.
Como en el ı́tem anterior, bastará demostrarlo para
A = (∀x1 ) . . . (∀xn )(∃y)B(x1 , . . . , xn , y)
Sea (u1 , . . . , un ) ∈ U n y sea ξ ′ una valuación de variables tal que ξ ′ (z) = ξ(z) si z ∈
/
{x1 , . . . , xn } y tal que
ξ ′ (x1 ) = u1 , . . . , ξ ′ (xn ) = un
Tenemos, pues, que Iξ ′ ((∃y)B(x1 , . . . , xn , y)) = 1. Luego existe una valuación de variables
′′
ξ que es y-equivalente a ξ ′ y tal que verifica la condición Iξ ′′ (B(x1 , . . . , xn , y)) = 1.
Sea f un sı́mbolo de función n-ario que no aparece en B (esto es posible debido a la
ampliación de L1 a L+ ′ ′ ′
1 ). Ahora, definimos M = (U, I ) tal que I difiere de I únicamente
′
en la interpretación de f y tal que I (f ) se define como sigue:
′′
I ′ (f )(u1 , . . . , un ) = ξ (y)
′′
es decir, Iξ′ ′ (f (x1 , . . . , xn )) = ξ (y), ası́ como Iξ′ ′′ (B(x1 , . . . , xn , y)) = 1, pues las interpre-
′′
taciones (U, I) y (U, I ′ ) comparten el mismo dominio, ası́ que ξ ′ y ξ son valuaciones de
variables asociadas a (U, I ′ ) igualmente.
Terminamos esta sección con la definición de una clase de fbfs que, como en el caso proposicional,
es usada frecuentemente en el campo de la demostración automática y en la programación lógica.
Definición 1.45 Una fbf A se dice que está en forma clausal si es una forma normal de
Skolem y su matriz es una forma normal conjuntiva.
Como en el caso proposicional, usaremos una notación más concisa escribiendo la matriz como
conjunto de cláusulas y omitiendo los cuantificadores (ya que sabemos que todos son universales)
Ejemplo 1.23 La forma clausal
(∀x)(∀y)(∀z) P (x) ∧ (Q(f (x, y) ∨ P (g(z))) ∧ (¬Q(x, z) ∨ ¬P (a))
Teorema 1.13 Para toda fbf A de L1 existe una forma clausal ACl tal que A y ACl son equi-
satisfacibles.
Ejemplo 1.24
es decir,
{¬P (x, f (x)) ∨ R(x, f (x), g(x)), Q(x, g(x)) ∨ R(x, f (x), g(x))}
Ahora el proceso para obtener una forma clausal requiere introducir un sı́mbolo de constante
y un sı́mbolo de función monaria (por ejemplo, los sı́mbolos a y g):
Para terminar este capı́tulo, introducimos la noción central en nuestro estudio, establecemos
qué entendemos por razonamiento correcto en la semántica de L1 .
La definición de consecuencia lógica para la lógica de primer orden fue dada por primera vez
por Tarski, aunque algunos trabajos previos de Bolzano y Hilbert hacen uso de ella.
1.5. CONSECUENCIA LÓGICA 43
Ω, A |= B si y sólo si Ω |= A → B
en particular,
A1 , A2 , . . . , An |= A si y sólo si |= (A1 ∧ A2 ∧ · · · ∧ An ) → A
si y sólo si |= A1 → (A2 → (A3 · · · → (An → A) . . .))
y también, tenemos
A1 , A2 , . . . , An |= A si y sólo si A1 ∧ A2 ∧ · · · ∧ An ∧ ¬A es insatisfacible
1. (∀x)A(x) |= (∃x)A(x)
2. (∃x)(∀y)A(x, y) |= (∀y)(∃x)A(x, y)
1.6. Ejercicios
1. Diga cuáles de las siguientes cadenas de sı́mbolos son fórmulas de un lenguaje de primer orden.
Para aquellas que sean fórmulas, construya su árbol sintáctico.
(∃x)(P (x) → Q(x, y)), (∃x)P (x) → Q(x, y), (∃x)P (y),
c) Todo el que plagia el trabajo ajeno es un inepto. De todos es sabido que los expertos en
programación no son ineptos y que algunos expertos en programación dominan las técnicas
de la programación paralela. Por lo tanto, algunos de los que dominan las técnicas de la
programación paralela, no plagian el trabajo ajeno.
d ) Todas las enfermedades infecciosas son controlables. Quien padece una enfermedad controla-
ble, o no se preocupa por la enfermedad o se automedica. Luis es un deportista que nunca
se automedica, pero que padece una enfermedad infecciosa. Por lo tanto, hay deportistas que
no se preocupan por la enfermedad que padecen.
e) Todo estudiante que deja la adquisición de conocimientos sobre una materia para la semana
antes del examen, tiene una disculpa interesante. Hay estudiantes aburridos cuyas disculpas
son aburridas. No hay aburridos interesantes. Ası́ pues, de lo dicho se concluye que no hay
quien preocupándose de adquirir conocimientos sobre una materia durante todo el curso, sea
aburrido.
f ) Las sustancias radioactivas tienen vida corta o un valor medicinal. Ningún isótopo del uranio
que sea radioactivo tiene vida corta. Por tanto, si todos los isótopos del uranio son radioac-
tivos, todos los isótopos del uranio tienen un valor medicinal.
7. Probar las siguientes equivalencias:
(∃y)(∀x)(P (x) ∧ Q(y)) ≡ (∀x)(∃y)(P (x) ∧ Q(y))
(∀x)(∃y) P (y) ∧ (Q(x) → R(y)) ≡ (∃y)(∀x) P (y) ∧ (Q(x) → R(y))
8. Dada la fbf
A = ¬(∀x) (∃y)P (x, y) ∨ ¬(∀z)Q(z, x) ∧ (∀t) R(t) → S(t)
a) Obtener el conjunto de las subfórmulas de A.
b) Obtener el conjunto de las subfórmulas que ocurren positivamente en A.
c) Obtener el conjunto de las subfórmulas que ocurren negativamente en A.
9. Sean las fbfs:
a) (∀x)P (y) → ¬P (x).
b) (∀x)(∀y)(Q(x, y, z) → (P (y) → ¬R(x))).
c) (∀x)¬(∀y)P (x) → S(x, y).
d ) (∀x)(∀y)(P (x) → S(x, y)) → ¬(∀y)Q(x, y, z).
Determinar para cada ocurrencia de un sı́mbolo de variable si es libre o ligada.
10. Hallar Vlibres para cada una de las fbfs siguientes:
a) (∀x)P (x, y) → P (x, a)
b) (∀x)(P (x, y) → P (x, a))
c) (∀x) (∃y)P (x, g(a, y)) → (∃z)P (y, z)
11. Especificar para cada una de las fbfs siguientes si el término f (x, z) es libre para x:
a) (∀y)(P (x, y) → P (y, a))
b) Q(z) → ¬(∀x)(∀y)R(x, y, a)
c) (∀x)Q(x) → (∀y)P (x, y)
d ) (∀y)(P (f (x, y), x) → E(z, g(x, y)))
12. Dados los términos h(x, y) y g(a, f (y, z)), determinar si son libres para cada una de las variable x,
y y z en las fbfs siguientes:
46 CAPÍTULO 1. LÓGICA DE PRIMER ORDEN
a) (∀z) P (z, y, a) ∧ (∀x)Q(g(x, z))
b) (∀x)R(f (x, a), y) → ¬R(f (x, a), z)
c) P (f (x, a), x, b) → ¬P (f (y, b), z, b)
13. Dados los términos f (x, u) y f (x, f (z, u)), determinar si son libres para cada una de las variable
x, y y u en las fbfs siguientes:
a) (∀x)P (x, y, z) → (∀z)P (z, x, u)
b) (∀y)P (y, f (x, y), z) → (R(x) → Q(u))
14. Evalúe las siguientes sustituciones
a) [x/f (y)]((∀x)P (x) → Q(x));
b) [y/f (y)]((∀x)(¬P (y) ∨ (∃y)Q(x, y)))
15. Hallar [x/f (x, z)]A para cada uno de los siguientes casos:
a) A = (∀y)P (y, f (x, y)) → Q(x)
b) A = (∀x)(∀z)(Q(z) → Q(x))
c) A = (∀y)Q(g(y)) → (∀z)R(x, y, z)
d ) A = (∀y)R(x, g(x), y) → (∀z)Q(f (x, z))
16. La composición de sustituciones no es conmutativa, y por eso una composición como [y/s] ◦ [x/t] se
evalua sobre una fórmula sustituyendo secuencialmente las variables: en primer lugar sustituimos
la variable x y posteriormente la variable y. Definimos la sustitución simúltánea de las variables
x1 ,. . . ,xn por los términos t1 ,. . . ,tn respectivamente y se denota como {x1 /t1 , . . . , xn /tn } como la
aplicación que, sobre una fórmula A sustituye simultáneamente todas las apariciones libres de las
variables x1 ,. . . ,xn por los términos t1 ,. . . ,tn respectivamente.
Evalúe la sustitución {x/g(y), y/g(x)}A(x, y) y deduzca que
21. Sea Σ = ({a, b, c}, {f, g}, {P, Q}) la signatura del conjunto de fbfs
Ω = {P (a), P (b), P (c), P (f (a)), P (f (b)), P (f (c)), P (g(a, b)), P (g(a, c)), P (g(b, c)), P (g(f (b), c)),
P (g(f (c), f (b))), (∀x)Q(x, x), (∃x)Q(x, f (x))}
Sea (U, I) una interpretación para L1 donde U = C ∗ , C es el alfabeto de la lengua española y
- I(a) = “la”
- I(b) = “ma”
- I(c) = “ireo”
- I(f )(d) = d si |d| = 1 y, en otro caso, el resultado de eliminar la primera letra en d. Por
ejemplo, I(f )(“hasta”) = “asta”.
- I(g) asocia a cada par (d, d′ ) la concatenación de d y d′ . Por ejemplo, I(g)(“por”, “cal”) =
“porcal”.
- I(P ) consiste en el conjunto de palabras de la lengua española. Por ejemplo, “topo” ∈ I(P ),
“opot” ∈/ I(P ).
- I(Q) consiste en el conjunto de pares (d, d′ ) tales que d es una subcadena de d′ . Por ejemplo,
(“amo”, “gamo”) ∈ I(Q), (“repta”, “paleta”) 6∈ I(Q).
Hallar I(A) para toda fbf A ∈ Ω.
22. Considere la siguiente interpretación (U, I): con U = N: I(a) = 0, I(f )(n, m) = n+m, I(g)(n, m) =
n · m e I(P ) es la relación de igualdad. Interprete las siguientes fbfs y determine si (U, I) es un
modelo para ellas:
(∀x)P (g(x, a), x) (∀x)(∀y)(P (f (x, a), y) → P (f (y, a), x))
(∀x)(∀y)(∃z)P (f (x, y), z) (∃x)P (f (x, x), g(x, x))
A = (∀x)(∀y)((P (y, x) ∧ (P (x, a) ∨ E(x, a))) → (P (a, f (x, y)) ∨ E(a, f (x, y)))
Determine si I es un modelo de A.
24. Sea Σ = ({a}, {f }, {P, E}) la signatura para la fbf
A = (∀x)(∀y)((P (y, x) ∧ (P (x, a) ∨ E(x, a))) → (P (a, f (x, y)) ∨ E(a, f (x, y)))
1) I ′ (a) = 2.
2) I ′ (f ) es la suma en Z3
3) I ′ (P ) = ≡3 , la relación de congruencia módulo 3.
4) I ′ (E) es la relación R definida como (n, m) ∈ I ′ (R) si y sólo si n + 1 ≡3 m.
Describir en lenguaje natural la información contenida en A por esta interpretación y hallar
I ′ (A).
26. Sea t un término básico, A una fbf, M = (U, I) una interpretación para L1 , x un sı́mbolo de
variable y ξ una valuación de variables asociada a (U, I).
Probar que para toda valuación ξ ′ que sea x-equivalente a ξ con ξ ′ (x) = I(t) se tiene que
36. Determinar cuáles de los siguientes conjuntos de fbfs son satisfacibles y, para cada uno de ellos,
dar un modelo:
a) {(∀x)(∃y)P (x, y), (∀x)¬P (x, x)}
b) {(∃x)(∀y)P (x, y), (∀x)¬P (x, x)}
c) {(∀x)(P (x) ∨ Q(x)), ¬(∃x)P (x), ¬Q(a)}
d ) {(∃x)(P (x), (∀x)(P (x) → Q(x)), (∀x)¬Q(x)}
e) {(∀x)(P (x) → (∃y)Q(x, y)), (∀x)(∀y)(Q(x, y) → R(y)), P (a) ∧ ¬R(a)}
37. Probar que {∧, ∨} y {↔, ∃} no son conjuntos adecuados de conectivas en L1 .
38. Si Mod(X) denota el conjunto de los modelos de la fbf X, expresar en términos de Mod(A) y
Mod(B) los siguientes conjuntos
a) Mod(A ∧ B)
b) Mod(A ∨ B)
c) Mod(A ∧ ¬B)
d ) Mod(A → B)
39. Sean A y B dos fbfs tales que Vlibres (A) = Vlibres (B) y sean A′ y B ′ sus cierres universales. Probar
que
A ≡ B si y sólo si A′ ≡ B ′
40. (Principio de dualidad) Demuestra que si en una equivalencia lógica en la que no intervienen las
conectivas → ni ↔ se intercambian ∧ y ∨; ∀ y ∃ se obtiene otra equivalencia lógica.
41. Obtener una forma normal prenexa lógicamente equivalente a la fbf A siguiente
(∀x) P (x) ∧ (∃y)(¬Q(x, y) ∨ (∀z)R(x, z)) ∧ ((∃y)¬R(x, u) ∨ Q(x, y))
50 CAPÍTULO 1. LÓGICA DE PRIMER ORDEN
42. Obtener una forma normal prenexa lógicamente equivalente para las fbfs siguientes
a) (∀x)P (x) → (∃x)Q(x)
b) (∀x)(∀y)[(∃x)(P (x, z) ∧ P (y, z)) → (∃u)Q(x, y, u)]
c) (∀x)[P (x) ∧ (∀y)(∃w)(¬Q(x, y) → (∀z)R(a, x, y))]
d ) (∀x)(∀y)[(∃z)P (x, y, z) ∧ ((∃u)(Q(x, u) → (∃v)Q(y, v))]
43. Transformar en forma clausal las fbfs siguientes
a) (∃x)P (x) → ( (∀x)(Q(x) ∨ S(x)) → (∀x)(∃y)R(x, y) )
b) (∀x)[¬P (x, a) → (∃y)(P (y, g(x)) ∧ (∀z)(P (z, g(x)) → P (y, z)))]
c) (∀x)(∀y)[(∃z)P (z) ∧ (∃u)(Q(x, u) → (∃v)q(y, v))]
44. Demostrar que son válidas las inferencias lógicas del Ejemplo 1.25
45. Demostrar que |= es un operador de consecuencia, es decir, si utilizamos la notación
para la aplicación tal que para cada Ω ∈ 2L1 se tiene que |= (Ω) es el conjunto de fbfs que son
consecuencia lógica de Ω, entonces |= satisface las siguientes propiedades:
(i) Ω ⊆ |= (Ω) (Inclusión)
(ii) |= (|= (Ω)) ⊆ |= (Ω) (Transitividad)
(iii) Si Ω ⊆ Γ, entonces |= (Ω) ⊆ |= (Γ) (Monotonı́a)
46. Dado un conjunto de fbfs Γ, una constante c y una fbf A con a lo sumo una variable libre x,
demuestre las siguientes afirmaciones:
a) si Γ |= A[x/c ], entonces Γ |= (∃x)A.
b) si Γ |= (∀x)A, entonces Γ |= A[x/c ]
c) si se tiene que
Γ |= (∃x)A,
Γ ∪ {A[x/c ]} |= B y
c no aparece en Γ ni en A ni en B,
entonces Γ |= B.
d ) si Γ |= A[x/c ] y c no aparece en Γ ni en A, entonces Γ |= (∀x)A.
47. Demuestre las siguientes equivalencias e inferencias
a) (∃x)(A(x) → B(x)) ≡ ((∀x)A(x) → (∃x)B(x))
b) (∀x)(A(x) → B(x)) |= ((∀x)A(x) → (∀x)B(x))
c) (∀x)(A(x) → B(x)) |= ((∀x)A(x) → (∃x)B(x))
d ) (∀x)(A(x) → B(x)) |= ((∃x)A(x) → (∃x)B(x))
e) (∃x)B(x) → (∀x)A(x) → (∀x)(A(x) → B(x))
Capı́tulo 2
Modelos de Herbrand
En este capı́tulo estudiamos un resultado fundamental de la lógica clásica de primer orden que,
como veremos, tiene especial interés en la semántica de los lenguajes de programación lógica:
El estudio de la satisfacibilidad de un conjunto de fbfs de la lógica clásica de primer
orden se puede reducir al estudio de la satisfacibilidad de un conjunto de cláusulas
básicas (es decir, cláusulas en las que no intervienen variables) que, en consecuencia,
puede ser contemplado como un conjunto de cláusulas de la lógica proposicional.
Comencemos con el siguiente análisis: Como venimos insistiendo, el conjunto de posibles in-
terpretaciones M = (U, I) en la lógica clásica de primer orden, incluso el conjunto de posibles
interpretaciones para una fbf, es extremadamente complejo, ya que requiere la elección del domi-
nio o universo del discurso, U , y para cada dominio U nos encontramos con la amplia variabilidad
para I, es decir, las interpretaciones para el conjunto de sı́mbolos de constantes, para el conjunto
de sı́mbolos de función y para el conjunto de sı́mbolos de predicados.
Es pues poco razonable afrontar a las bravas la tarea de determinar si una fbf A es o no válida,
incluso limitándonos a formas normales, pues necesitarı́amos comprobar que A es verdadera en
toda interpretación M = (U, I).
Afortunadamente, se dispone de una teorı́a que simplifica drásticamente el conjunto de inter-
pretaciones que se necesita considerar, esta teorı́a se debe a Jacques Herbrand y, como veremos,
permite el estudio de la demostración automática de teoremas limitándonos a considerar inter-
pretaciones con dominios uniformes. Además, lo que es más importante, estas interpretaciones
se definen sintácticamente en términos de los sı́mbolos del lenguaje, con la simplicidad que ello
conlleva.
Los resultados estudiados en este capı́tulo son quizás los más relevantes de la lógica; sin ellos
no hubiera sido posible abordar la tarea de obtener razonadores automáticos aceptablemente
eficientes y, en consecuencia, de hacer de la lógica una herramienta útil para las Ciencias de la
Computación.
Comenzamos introduciendo el concepto básico en esta teorı́a, el dominio uniforme anunciado
anteriormente.
Definición 2.1 Dado un lenguaje de primer orden L1 (C, F, P), se llama universo de Her-
brand de L1 (C, F, P), denotado HL1 :
al conjunto de términos básicos de L1 (C, F, P), si C 6= ∅ y, en caso contrario,
52 CAPÍTULO 2. MODELOS DE HERBRAND
1. c ∈ HΩ
2. Si f es un sı́mbolo de función n-aria que ocurre en Ω y t1 , . . . , tn ∈ HΩ entonces
f (t1 , . . . , tn ) ∈ HΩ
HΩ es finito si y sólo si FΩ = ∅
Como para todo conjunto inductivo libremente generado, si Ω es finito y HΩ es infinito, podemos
considerar HΩ como una unión numerable de conjuntos finitos:
[
HΩ = Hi,Ω
i∈N
donde
2. Para i > 0 definimos Hi+1,Ω como la unión de Hi,Ω y el conjunto de términos de la forma
f (t1 , . . . , tn ) para todo sı́mbolo de función n-aria que ocurre en Ω y toda n-upla de términos
(t1 , . . . , tn ) en Hi,Ω .
De esta forma, podemos decir que el mérito de Herbrand es haber logrado tender un puente
entre lo finito y lo infinito gracias a la idea de contemplar un dominio infinito (numerable)
como una sucesión de dominios finitos. Esta sucesión puede contemplarse como una sucesión de
aproximaciones a este dominio infinito.
¿Qué ocurre con la segunda componente de (U, I)? también en esta componente podemos limi-
tarnos a considerar el conjunto de enunciados atómicos sobre los individuos representados por
los elementos de HΩ . Este conjunto se describe mediante la siguiente definición:
Definición 2.3 Sea Ω un conjunto de cláusulas y PΩ el conjunto de sı́mbolos de predicados que
intervienen en Ω. La base de Herbrand de Ω, denotada BΩ , se define como el conjunto de
átomos básicos generados por PΩ y HΩ , es decir, el conjunto de átomos de la forma siguiente:
Si P ∈ PΩ es un sı́mbolo de predicado n-ario y t1 , . . . , tn ∈ HΩ , entonces P (t1 , . . . , tn ) ∈ BΩ .
Definición 2.4 Dado un conjunto de cláusulas, Ω, se llama instancia básica de una cláusula
C ∈ Ω a una cláusula obtenida reemplazando las variables de C por elementos de HΩ .
Definición 2.5 Sea Ω un conjunto de cláusulas. Una interpretación para Ω se dice que es una
interpretación de Herbrand, denotada MH,Ω si es de la forma (HΩ , IH,Ω ) cuyo dominio es
54 CAPÍTULO 2. MODELOS DE HERBRAND
el universo de Herbrand para Ω y donde IH,Ω asocia cada sı́mbolo de constante y a cada sı́mbolo
de función el propio sı́mbolo, es decir,
en definitiva, si (HΩ , IH,Ω ) es una interpretación de Herbrand, para todo término básico t se
tiene que
IH,Ω (t) = t.
r r Herbrand afirma que basta interpretar sintácticamente tanto los sı́mbolos de constante como
ee
los sı́mbolos de función; ası́, por ejemplo, tenemos que
Destaquemos también que, por definición, una valuación de variables ξ asociada a una in-
terpretación de Herbrand es también una sustitución (ya que asigna a cada variable un
término).
Por su propia definición, dos interpretaciones de Herbrand para Ω sólo difieren en la interpreta-
ción de los sı́mbolos de predicado. En consecuencia:
Toda interpretación de Herbrand queda determinada por un subconjunto de la base de
Herbrand, BΩ , concretamente: el conjunto de átomos básicos a los que IH,Ω asigna
el valor de verdad 1. En consecuencia, el cardinal del conjunto de interpretaciones
de Herbrand para Ω es el cardinal del conjunto de subconjuntos de BΩ , es decir, 2ℵ0 .
({1, 2}; {a ; 1}; {f ; {(1, 2), (2, 2)}}; {P ; {1}, Q ; {2}, R ; {2}})
2.1. INTERPRETACIONES DE HERBRAND 55
Ejemplo 2.2
2. Para Ω2 = {P (x, f (y)) ∨ ¬Q(y, x), ¬P (z, u) ∨ Q(u, u)} se tiene que
Podemos ya establecer el resultado fundamental que nos muestra la utilidad de los modelos de
Herbrand.
∗
IH,Ω = {P (t1 , . . . , tn ) ∈ BΩ | (I(t1 ), . . . , I(tn )) ∈ I(P )}
∗
Veamos que IH,Ω satisface Ω:
Por ser (U, I) un modelo para Ω, si C es una cláusula de Ω y Var (C) = {x1 , . . . , xn } se tiene
que I((∀x1 ) . . . (∀xn )C(x1 , . . . , xn )) = 1. Por lo tanto, para toda n-upla de términos básicos
(t1 , . . . , tn ) se tiene que I(C(t1 , . . . , tn )) = 1, es decir, para toda cláusula C ∈ Ω y para toda
instancia básica C b de C se tiene que I(C) = 1 y por lo tanto existe un literal básico lib en C b
56 CAPÍTULO 2. MODELOS DE HERBRAND
Bueno, es cierto que un segundo es mucho tiempo para una computadora, y que en
ese tiempo es posible que realice miles de operaciones y no una sola operación co-
mo dijimos arriba. Consigamos entonces una supercomputadora que pueda realizar
un millón de pasos por segundo. Quizás ahora ¿no tendrı́amos problemas? No lo
tendrı́amos en el ejemplo que consideramos antes (que resolverı́amos en sólo 0,1 se-
gundos), pero consideremos una fórmula de tamaño 10, y un modelo de 25 elementos.
Entonces:
C (como PSpace o ExpTime) quiere decir que existe alguna instancia del problema
que requiere tanto espacio o tiempo. Podrı́an haber muchas otras instancias mucho
mas simples.
Y aquı́ es donde el tema se pone interesante. Seguramente en una aplicación dada
no usaremos todo el poder expresivo de la lógica clásica de primer orden. ¿Quizás es
posible elegir fragmentos más simples y que de todas formas tengan la expresividad
necesaria para nuestra aplicación?
En efecto, ciertos fragmentos de la lógica clásica de primer orden son decidibles. Por ejemplo, la
clase de las fórmulas válidas de L1 en la que no intervienen sı́mbolos de función y en la que todos
los sı́mbolos de predicado que intervienen son monarios. También lo es el conjunto de fbfs con a
lo sumo 2 variables, es decir, en las que pueden aparecer a los sumo los sı́mbolos de variable x1
y x2 (tanto si consideramos la lógica clásica de primer orden con igualdad o sin ella), denotado
LP O2 .4
La mayorı́a de las clases decidibles son clases de fórmulas prenexas que se definen sintácticamente
mediante restricciones sobre la estructura del prefijo, restricciones sobre su matriz o restricciones
sobre ambos. Destaquemos algunas:
1. Sea A una fórmula en fnp en la que no intervienen sı́mbolos de función. Entonces, existe
un procedimiento de decisión para la satisfacibilidad de A si el prefijo de A tiene una de
las formas siguientes:
2. Sea A una fórmula en fnpc. Entonces existe un procedimiento de decisión para la satisfa-
cibilidad de A si la matriz de A es de una de las siguientes formas:
Teorema 2.2 La Lógica Clásica de Predicados de Primer Orden no es decidible pero sı́ es
semidecidible, es decir, existen algoritmos tales que: dada una fórmula A, si esta fórmula es
válida, el algoritmo determina su validez tras una secuencia finita de pasos; si la fórmula no es
válida, el algoritmo puede finalizar con esta conclusión tras una secuencia finita de pasos o no
terminar.
Cada arco de profundidad k está etiquetado con el literal Pk o con el literal ¬Pk donde
Pk ∈ ∆.
Los literales que etiquetan dos arcos que nacen del mismo nodo son opuestos.
Cada Pi ∈ ∆ ocurre en cada rama a lo sumo una vez (bien como etiqueta Pi o bien como
etiqueta ¬Pi ).
El valor 1 si un arco del camino que une N con la raı́z está etiquetado por el literal P .
El valor 0 si un arco del camino que une N con la raı́z está etiquetado por el literal ¬P ,
! !!•aa
aa
!!
P (a) ¬P (a)
! aa
! !! aa
a•
I1H (P (a)) =1H
•
HH I8H (P (a)) = 0
P (b) H¬PH
(b)
I2H (P (b)) = 1 HH I5H (P (a)) = 1
I2H (P (a)) = 1 • • I5H (P (b)) = 0
@ @
Q(a, b) @ ¬Q(a, b) Q(a, b) @ ¬Q(a, b)
@@• @@•
• •
I3H (P (a)) = 1 I4H (P (a)) = 1 I6H (P (a)) = 1 I7H (P (a)) = 1
I3H (P (b)) = 1 I4H (P (b)) = 1 I6H (P (b)) = 0 I7H (P (b)) = 0
I3H (Q(a, b)) = 1 I4H (Q(a, b)) = 0 I6H (Q(a, b)) = 1 I7H (Q(a, b)) = 0
Ejemplo 2.4 El árbol de la Figura 2.1 es un árbol semántico respecto a ∆ = {P (a), P (b), Q(a, b)}.
!!•aa
R(a) !!! aa ¬R(a)
! aa
!! aa
•!
a
•H I2H (A) =?
HH
I1H (A) = 0 P (a) H¬P (a)
H
H
I3H (A) =? • H•
@
@ ¬Q(a) I4H (A) = 0
Q(a)
@
@•
•
I5H (A) = 0 I6H (A) = 0
donde A = (¬P (a) ∨ Q(a)) ∧ (¬Q(a) ∨ R(a)) ∧ P (a) ∧ ¬R(a). Por lo tanto, el razonamiento es
válido.
Veamos qué ocurre cuando HΩ es infinito.
Definición 2.9 Un nodo N de un árbol semántico para Ω respecto de una enumeración ∆ =
{P1 , P2 , . . . , Pn , . . .} de los átomos de BΩ se denomina nodo fallo si la interpretación parcial de
Herbrand IH asociada a N es tal que I(Cib ) = 0 para alguna instancia básica de una cláusula Ci
de Ω, pero ninguna de las interpretaciones parciales de Herbrand asociadas a sus ascendientes
posee esta propiedad.
Un nodo fallo nos proporciona una interpretación (parcial) de Herbrand IH que hace falsa a Ω.
Por lo tanto, no es preciso considerar las extensiones de I. De aquı́ la definición siguiente.
Definición 2.10 Un árbol semántico respecto de ∆ = {P1 , P2 , . . . , Pn , . . .} se dice cerrado si
todas sus hojas son nodos fallo.
Ejemplo 2.6 Dado Ω = {P (x), ¬P (x)∨Q(f (x)), ¬Q(f (a))}, la figura muestra un árbol semánti-
co cerrado para Ω respecto de la sucesión
!!•aa
P (a) !!! aa
¬P (a)
! aa
!! aa
•!
(∗) H a•
H
HH¬Q(f (a)) I4H (P (a)) = 0
Q(f (a)) HH
• H•
I2H (¬Q(f (a)) = 0 I3H (¬P (a) ∨ Q(f (a)) = 0
El teorema de Herbrand admite otro enunciado equivalente que no utiliza el concepto de árbol
semántico y que es mencionado habitualmente en la literatura como teorema fundamental
de Herbrand:
Teorema 2.5 Un conjunto de cláusulas, Ω, es insatisfacible si y sólo si existe un conjunto finito
de instancias básicas de cláusulas de Ω que es insatisfacible.
Podrı́amos decir, que el teorema de Herbrand permite desarrollar la semántica de la lógica de pri-
mer orden utilizando únicamente medios sintácticos. Por otra parte, el teorema fundamental de
Herbrand es un teorema de compacidad sintáctica y, como veremos a continuación, proporciona
un semialgoritmo para el estudio de la satisfacibilidad en la lógica de primer orden:
2.2. TEOREMA DE HERBRAND Y SEMIDECIDIBILIDAD DE L1 63
∆ = {C1 , . . . , Cn , . . .}
es satisfacible. En efecto, (N, {a ; 0}, {f ; {(n, n + 1)}, {P ; R}) es un modelo para A. Sin
embargo, como veremos, A no es válida:
Una forma clausal simultáneamente satisfacible con ¬A es
Ejemplo 2.8 Vamos a estudiar la validez de una inferencia utilizando el principio de refutación
y el algoritmo de Gilmore sobre la base de Herbrand de la fórmula obtenida tras hallar una
fórmula en forma normal de Skolem a partir de la refutación:
Dado que S no contiene funciones, el universo de Herbrand está formado simplemente por las
constantes, HS = {a, b}, y la base de herbrand es finita, BS = {P (a), Q(a), P (b), Q(b)}.
Llamemos A1 = (∀x)(∀y)(P (y) → Q(x)) y A2 = ¬(P (b) → Q(a)).
Para entender mejor el árbol que construimos a continuación, es conveniente observar que los
modelos de Herbrand de A1 = (∀x)(∀y)(P (y) → Q(x)) coinciden con los de la fórmula
las dos fórmulas no son lógicamente equivalentes, pero sı́ son equivalentes en el universo de
Herbrand.
Ejemplo 2.9 Aunque el universo de Herbrand sea infinito, si la inferencia es válida, siempre
podremos encontrar un árbol finito que lo demuestre.
El universo de Herbrand es
y la base de Herbrand es
Llamemos A1 = (∀x)P (x), A2 = (∀x)(P (x) → Q(f (x))) y A3 = ¬Q(f (a)) para construir el
árbol de Gilmore.
BS = {P (a), P (b), Q(a), Q(b), D(a), D(b), L(a, a), L(a, b), L(b, a), L(b, b)}
Demostración: Basta considerar el Teorema 2.1 y que el universo de Herbrand para el conjunto
de cláusulas simultáneamente insatisfacible con Γ generado por el procedimiento introducido en
la Sección 1.4 es finito.
En cuanto a los modelos infinitos, tenemos los resultados siguientes.
Teorema 2.7 (de Löwenheim) Si una fórmula A es satisfacible entonces tiene un modelo
numerable.
Demostración: Puesto que todo lenguaje de primer orden es numerable, cualquier conjunto Ω
considerado es numerable. Si Ω es infinito numerable, sea Ω = {Ai | i ∈ N}, podemos considerar
para cada fórmula Ai ∈ Ω una forma clausal Γi simultáneamente satisfacible con Ai y tal que los
conjuntos de constantes y de funciones de Skolem asociados a ellas son disjuntos dos a dos. Por lo
tanto, podemos considerar el conjunto Γ = {Γi | i ∈ N} que es simultáneamente satisfacible con
Ω. Ahora, el Teorema 2.1 asegura la existencia de un modelo de Herbrand, que es obviamente
numerable.
2.4. INDECIDIBILIDAD DE L1 67
2.3.1. Compacidad
Como un corolario destacado más, en esta sección estudiamos el teorema de compacidad, que
caracteriza la satisfacibilidad de un conjunto infinito de fórmulas.
Teorema 2.9 (de compacidad) Un conjunto de fbfs de L1 , Ω, es satisfacible si y sólo si es
finitamente satisfacible, es decir, todo subconjunto finito es satisfacible.
2.4. Indecidibilidad de L1
El problema siguiente se conoce como problema de la correspondencia de Post:
Dada una secuencia [(a1 , b1 ), . . . , (ak , bk )] de pares de palabras no vacı́as sobre el
alfabeto {0, 1}, encontrar una secuencia de ı́ndices [i1 , . . . , in ] tal que ai1 . . . ain =
bi 1 . . . bi n .
A una secuencia de este tipo se le denomina una solución del problema de correspondencia
[(a1 , b1 ), . . . , (ak , bk )].
Ejemplo 2.11 Para el problema de correspondencia
[(1, 101), (10, 00), (011, 11), (1001, 111)]
una solución es la secuencia 1, 3, 2, 3 ya que a1 a3 a2 a3 = 101110011 = b1 b3 b2 b3
Definición 2.13 Sean ∆1 y ∆2 dos conjuntos de palabras sobre un alfabeto finito Γ. Decimos
que ∆1 es reducible a ∆2 si existe una aplicación Φ : Γ∗ −→ Γ∗ tal que:
(i) Φ es decidible, es decir existe un algoritmo que proporciona Φ(γ) para toda entrada γ ∈ Γ∗ .
γ ∈ ∆1 si y sólo si Φ(γ) ∈ ∆2
Teorema 2.12 (de indecidibilidad de Church) Sea L1 un lenguaje de primer orden cuya
signatura es Σ = ({c}, {f, g}, {P }) donde f y g son sı́mbolos de funciones monarias y P es un
sı́mbolo de predicado binario. Entonces el conjunto de fórmulas válidas es un conjunto indecidi-
ble.
2.5. EJERCICIOS 69
2.5. Ejercicios
1. Dado un lenguaje de primer orden L1 con signatura ({c}, ∅, {P }), donde P es un sı́mbolo de
predicado monario, determinar su universo de Herbrand, HL1 .
2. Sea A(x1 , . . . , xn ) una fbf en la que no intervienen ni sı́mbolos de función ni sı́mbolos de cuanti-
ficación. Demostrar que (∀x1 ) . . . (∀xn )A(x1 , . . . , xn ) tiene un modelo si y sólo si tiene un modelo
cuyo dominio consta de un único elemento.
3. Dada la fórmula A = (∃x)(P (x) → (∀y)P (y)),
a) Hallar un conjunto de cláusulas, Ω, simultáneamente satisfacible con A.
b) Hallar HΩ y BΩ .
c) Probar que A es válida.
4. Dada la fórmula A = (∃x)P (x) → Q(a) ∧ ¬(∀y)R(y) ∧ (∃y)D(y)
a) Hallar un conjunto de cláusulas Ω simultáneamente satisfacible con A.
b) Hallar HΩ y BΩ .
c) Dar, si existe, un modelo de Herbrand para Ω.
5. Hallar HΩ y BΩ para un conjunto de cláusulas simultáneamente satisfacible con el conjunto de fbfs
16. Dada la fórmula A = (∃x)(P (x) → (∀y)P (y)), halle un conjunto Ω de fórmulas en forma normal de
Skolem tal que Ω sea satisfacible si y solo si lo es A. Determine el universo y la base de Herbrand
de Ω y estudie la satisfacibilidad y la validez de A utilizando el método de Gilmore.
17. Estudie la validez de la siguientes inferencias utilizando el método de Gilmore:
(∃x)(P (x) ∧ (∀y)(D(y) → L(x, y)))
a) (∀x)(P (x) → (∀y)(Q(y) → ¬L(x, y)))
(∀x)(D(x) → ¬Q(x))
(∀x)(∀y)(∀z)((P (x, y) ∧ P (y, z)) → A(x, z))
b) (∀x)(∃y)P (y, x)
(∀x)(∃y)A(y, x)
72 CAPÍTULO 2. MODELOS DE HERBRAND
Capı́tulo 3
En este capı́tulo introducimos la extensión a la lógica de primer orden de los sistemas deductivos
considerados para la lógica proposicional en el primer volumen, es decir:
un sistema axiomático, y
Puesto que, como hemos analizado, la lógica de primer orden es una extensión de la lógica
proposicional, tan sólo requeriremos (en ambos casos) añadir a los axiomas y/o reglas de infe-
rencias de los sistemas proposicionales nuevos axiomas y/o reglas de inferencias para regir el
comportamiento de los cuantificadores.
Ax 1. A → (B → A)
Ax 3. (¬A → ¬B) → (B → A)
Los tres primeros axiomas son los axiomas del sistema de Lukasiewicz para la lógica
proposicional.
(∀x)(P (x) → Q(x)) → (P (x) → Q(t)) no es una instancia del Axioma 4, ya que la
sustitución de x por t no se ha realizado correctamente.
74 CAPÍTULO 3. SISTEMAS DEDUCTIVOS PARA L1
(∀x)(∃y)P (x, y) → (∃y)P (y, y) no es una instancia del Axioma 4, porque y no es libre
para x en (∃y)P (x, y).
Si en el Axioma 4 consideramos t = x tenemos como esquema de axiomas
(∀x)A(x) → A(x)
Reglas de inferencia:
A, A → B
Modus Ponens (MP):
B
A
Generalización (Gen):
(∀x)A
ee
rr Es importante advertir la diferencia entre el Axioma 4 y la regla de generalización: El
Axioma 4 asegura que de (∀x)A(x) se infiere en un único paso A(t) (si t es libre para
x en A(x)), por su parte, la regla de generalización (puesto que L1 es, como veremos,
correcto) recogerá el hecho de que “si A es válida entonces también lo es (∀x)A(x)” .
Veamos que la restricción en el Axioma 4 es necesaria: Si no exigimos que t sea libre
para x en A(x), la fbf siguiente serı́a un axioma
(∀x)(∃y)P (x, y) → (∃y)P (y, y)
Sin embargo, esta fbf no es válida; para comprobarlo, consideremos una interpretación
(U, I) cuyo dominio U tenga al menos dos elementos y tal que I(P ) = {(u, u′ ) ∈ U × U |
u 6= u′ }, entonces se tiene que I((∀x)(∃y)P (x, y)) = 1 y se tiene que I((∃y)P (y, y)) = 0.
Por lo tanto, el sistema no serı́a correcto ya que no todos los axiomas serı́an fbfs válidas.
Análogamente, si quitamos la restricción en el Axioma 5 de que x no sea una variable
libre en A, tendrı́amos como axioma, por ejemplo, la fbf
(∀x)(P (x) → P (x)) → (P (x) → (∀x)P (x))
¡Pero esta fbf no es válida. En efecto, en la interpretación (U, I) con dominio U = Z y
tal que I(P ) =“ser par” , se tiene I((∀x)(P (x) → P (x))) = 1; sin embargo, I(P (x) →
(∀x)P (x)) 6= 1 ya que, si tomamos la asignación de variables ξ definida por ξ(x) = 2
para todo sı́mbolo de variable x, se tiene Iξ (P (x)) = 1 y si tomamos la asignación de
variables ξ ′ definida por ξ ′ (x) = 3 y ξ ′ (y) = 2 para todo sı́mbolo de variable y 6= x,
tenemos que Iξ ((∀x)P (x)) = 0 y Iξ (P (x) → (∀x)P (x)) = 0. Por lo tanto, el sistema no
serı́a correcto.
Definición 3.1 Una fbf A se dice que es un teorema de L1 , si existe una secuencia finita de
fbfs, A1 , A2 , . . . , An tal que:
Cada Ai , donde 1 ≤ i ≤ n, es un axioma, o una fbf obtenida mediante la aplicación de
(MP) a partir de dos fórmulas anteriores en la secuencia o bien obtenida mediante la
aplicación de (Gen) a una fórmula anterior en la secuencia.
An es A.
La secuencia A1 , A2 , . . . , An se dice que es una demostración de A en L1 . Obviamente, todo
axioma es un teorema.
Definición 3.2 Dado un conjunto Ω de fórmulas, se dice que A es deducible o derivable en
L1 a partir de Ω, denotado Ω ⊢ A, si existe una secuencia finita de fórmulas A1 , A2 , . . . , An tal
que:
3.1. UN SISTEMA AXIOMÁTICO PARA L1 75
Puesto que L1 incluye todos los axiomas de la lógica proposicional y la regla de inferencia (MP),
tenemos obviamente el siguiente resultado
Teorema 3.1 Si A es una fbf de L1 que es un esquema de teorema de L, es decir, si A es una
tautologı́a de L1 , entonces A es un teorema de L1 y puede ser demostrada usando Ax.1, Ax.2,
Ax.3 y (MP).
Si Ω, A ⊢ B entonces Ω ⊢ A → B
es también cierto en el sistema L1 . Las restricciones (necesarias como nos muestra el siguiente
ejemplo) habrán de ser impuestas, como era de esperar, en el uso de la regla de generalización.
Ejemplo 3.2 Si no imponemos restricciones, puesto que tenemos A ⊢ (∀x)A, el teorema de
la deducción permitirı́a concluir que ⊢ A → (∀x)A. Claramente, no deseamos esto, ya que el
esquema A → (∀x)A no es un esquema válido.
En efecto, sea A = P (x) y sea (U, I) una interpretación con U = Z, I(P ) = “es igual a 0” ,
veamos que P (x) → (∀x)P (x) no es verdadera en esta interpretación; para ello basta encontrar
una asignación de variables, ξ, tal que Iξ (P (x) → (∀x)P (x)) = 0. Podemos considerar ξ tal
que ξ(x) = 0, con lo que Iξ (P (x)) = 1. Por otra parte existen valuaciones ξ ′ x-equivalentes a ξ
tales que Iξ ′ (P (x)) = 0. Por lo tanto, Iξ ′ ((∀x)P (x)) = 0 y Iξ ′ (P (x) → (∀x)P (x)) = 0. Ası́ pues
P (x) → (∀x)P (x) no es válida.
{A → B, B → C} ⊢ A → C
Los siguientes ejemplos ilustran el uso del teorema de la deducción para probar dos teoremas
del sistema L1 .
Ejemplo 3.3 Veamos que la fbf (A → (∀x)B) → (∀x)(A → B) es un teorema de L1 . Conside-
remos la siguiente deducción:
Hemos probado que A → (∀x)B ⊢ (∀x)(A → B). Puesto que x no es libre en (∀x)(A → B),
aplicando el teorema de la deducción se concluye que la fórmula (A → (∀x)B) → (∀x)(A → B)
es un teorema.
78 CAPÍTULO 3. SISTEMAS DEDUCTIVOS PARA L1
Hemos probado que (∀x)(A → B), (∀x)A ⊢ (∀x)B. Como (∀x)A es cerrada, por el teorema de
la deducción se tiene (∀x)(A → B) ⊢ (∀x)A → (∀x)B. Aplicando nuevamente el teorema de la
deducción, concluimos la prueba de que la fórmula (∀x)(A → B) → ((∀x)A → (∀x)B) es un
teorema.
Por lo tanto, (∀x)(∀y)A(x, y) ⊢ (∀y)(∀x)A(x, y). Como (∀x)(∀y)A(x, y) es cerrada, por el teore-
ma de la deducción se tiene
⊢ (∀x)(∀y)A(x, y) → (∀y)(∀x)A(x, y)
Si ⊢ A entonces |= A
Demostración: Por el Teorema 3.1, sabemos que los Axiomas 1, 2 y 3 son fbfs válidas.
El Axioma 4 es válido: Sea M = (U, I) una interpretación y ξ una valuación de variables
arbitraria asociada a M.
Tenemos que probar que, si el término t es libre para la variable x en la fórmula A, se tiene que
Iξ ((∀x)A(x) → A(t)) = 1.
Si Iξ ((∀x)A(x)) = 0 entonces Iξ ((∀x)A(x) → A(t)) = 1. Si Iξ ((∀x)A(x)) = 1 entonces, para toda
valuación de variables ξ ′ x-equivalente a ξ, se tiene que Iξ ′ (A(x)) = 1. En particular, podemos
3.1. UN SISTEMA AXIOMÁTICO PARA L1 79
elegir ξ ′ de modo que ξ ′ (x) = ξ(t). Por lo tanto, por ser t libre para x en A, Iξ (A(t)) = 1 y,
consecuentemente, Iξ ((∀x)A(x) → A(t)) = 1. Ası́ pues, I((∀x)A(x) → A(t)) = 1.
El Axioma 5 es válido: Es inmediato ya que, puesto que si una variable x no es libre en A,
se tiene que (∀x)(A → B(x)) ≡ (A → (∀x)B(x)).
Por último, es obvio que tanto (MP) como (Gen) respetan la validez, es decir:
Finalmente, probada la validez de los axiomas y que las reglas de inferencia preservan la validez,
mediante un argumento inductivo muy sencillo terminamos la demostración de que todo teorema
de L1 es una fbf válida.
Si |= A entonces ⊢ A
Teorema 3.6 (de consistencia) L1 es consistente, es decir, no existe ninguna fórmula A tal
que ⊢ A y ⊢ ¬A.
h : L1 −→ Lprop
definida como sigue: Para cada fórmula A de L1 , h(A) es la fórmula de la lógica clásica proposi-
cional, Lprop , obtenida al eliminar en A todos los cuantificadores y todos los términos y además
sustituir los sı́mbolos de predicado por el correspondiente sı́mbolo en minúscula de Lprop (junto
con la eliminación de las comas y paréntesis asociados a los cuantificadores, términos y átomos).
Por ejemplo:
Veamos que si A es un teorema de L1 , entonces h(A) es una tautologı́a de Lprop . Para ello
tendremos probar que:
- Si aplicamos una regla de inferencia a fbfs tales que sus imágenes por h son tautologı́as,
entonces la imagen por h de la fbf proporcionada por la regla de inferencia también es una
tautologı́a:
80 CAPÍTULO 3. SISTEMAS DEDUCTIVOS PARA L1
hipótesis
Conclusión
An es A.
A
A∧B A∧B
(∧, i) B (∧, e1 ) (∧, e2 )
A B
A∧B
A A
(→, i) B (→, e) A→B
A→B B
82 CAPÍTULO 3. SISTEMAS DEDUCTIVOS PARA L1
A∨B
A B A B
(∨, i1 ) (∨, i2 ) (∨, e)
A∨B A∨B C C
C
B
A ¬¬A
(¬, i) (¬e)
¬B A
¬A
Disponemos además de reglas de introducción y eliminación de cada uno de los cuantificadores:
(∀x)A(x)
donde t es un término libre para x en A(x).
A(t)
La lectura de esta regla es la siguiente:
Si sabemos que todo elemento del dominio es A, entonces sabemos que, en particular,
todo elemento expresado por t es A.
Para probar la corrección de (∀, e) tenemos que probar que, si t es un término libre para x en
A(x), entonces (∀x)A(x) → A(t) es válida. Pero este esquema es el Axioma 4 del sistema L1
dado en la sección anterior y su corrección la hemos probado en el Teorema 3.4.
Como para el Axioma 4 del sistema de Lukasiewicz, si no aseguramos las restricciones impuestas
a t, podemos llegar a conclusiones erróneas como nos muestra el siguiente ejemplo:
Ejemplo 3.6 La aplicación incorrecta de (∀, e) nos llevarı́a a deducir
1. Subderivación
A(x)
(∀x)A(x)
donde x es un sı́mbolo de variable que satisface las siguientes condiciones:
3.2. DEDUCCIÓN NATURAL 83
Ejemplo 3.8 Demostramos que (∀x)(P (x) ∧ Q(x)) ⊢DN (∀x)P (x) ∧ (∀x)Q(x)
1. (∀x)(P (x) ∧ Q(x)) hipótesis
Ejemplo 3.9 Demostramos que (∀x)(P (x) → Q(x)) ⊢DN (∀x)P (x) → (∀x)Q(x)
1. (∀x)(P (x) → Q(x)) hipótesis
2. Subderivación
Si no nos aseguramos de las restricciones impuestas a x en la regla (∀, i), podemos llegar a
conclusiones erróneas como nos muestra el siguiente ejemplo:
Ejemplo 3.10 La aplicación incorrecta de (∀, i) nos llevarı́a a probar
1. Subderivación
A[x/t]
(∃x)A(x)
donde t es un término libre para x en A(x). La lectura de esta regla es como sigue:
Para probar la corrección de (∃, i) tenemos que probar que A(t) → (∃y)A(x) es válida. Puesto
que (∃x)A(x) ≡ ¬(∀x)¬A(x), se tiene que
¬(∀x)A(x)
(∃x)¬A(x)
Demostración:
1. ¬(∀x)A(x) hipótesis
2. Subderivación
Análogamente se obtienen las siguientes reglas derivadas cuya demostración se deja al lector.
(∃x)¬A(x)
¬(∀x)A(x)
¬(∃x)A(x)
(∀x)¬A(x)
(∀x)¬A(x)
¬(∃x)A(x)
1. Subderivación
3.3. TEORÍAS DE PRIMER ORDEN 87
3. Subderivación
1. T es satisfacible.
Teorema 3.8 Sea I0 un conjunto no vacı́o de interpretaciones para un lenguaje de primer orden
L1 y sea FI0 el conjunto de fbfs en L1 tales que toda interpretación (U, I) ∈ I0 es un modelo de
FI0 . Entonces FI0 es una teorı́a de primer orden.
2. Los esquemas de axiomas del sistema de Lukasiewicz L1 , llamados axiomas lógicos, que
son independientes de la signatura especı́fica y que, como hemos analizado, son válidos en
toda interpretación M.
Una teorı́a de primer orden sin axiomas propios se denomina un cálculo de predicados de primer
orden. Por lo tanto, el calculo de predicados es universal en el sentido de que sus axiomas y
reglas de inferencia son comunes a todas las teorı́as de primer orden.
Definición 3.8 Un modelo para una teorı́a axiomática de primer orden T , es una interpre-
tación para la que todos los axiomas de T son válidos.
Puesto que las reglas de inferencia (MP) y (Gen) respetan la validez, podemos afirmar que:
Ejemplo 3.15 Definamos una teorı́a que describa todos los conjuntos estrictamente ordenados.
La signatura de tal teorı́a será tal que
Todos los átomos son de la forma x < y, donde x e y son sı́mbolos de variables.
2. Para recoger la semántica de E, esta teorı́a dispone de los siguientes axiomas propios:
Sin embargo, como nos muestra el siguiente ejemplo, los axiomas (E1 )–(E5 ) no garantizan que
en todo modelo de T = la interpretación de E sea “la identidad” sino tan sólo una “relación de
equivalencia” .
Ejemplo 3.16 Consideremos el lenguaje de primer orden cuya signatura consiste en un sı́mbolo
de función binario f y un sı́mbolo de predicado binario E. Consideremos la interpretación
(E1 ) (∀x)(x ≡2 x)
90 CAPÍTULO 3. SISTEMAS DEDUCTIVOS PARA L1
(E2 ) (∀x)(∀y)(x ≡2 y → y ≡2 x)
(E3 ) (∀x)(∀y)(∀z) (x ≡2 y ∧ y ≡2 z) → x ≡2 z
(E4 ) t ≡2 u → ((x + t) ≡2 (x + u))
(E5 ) t ≡2 u → (x ≡2 t → x ≡2 u)
Definición 3.10 Un modelo M = (U, I) de una teorı́a de primer orden con igualdad T = en el
que la interpretación de E es la identidad de U se dice que es un modelo normal.
Teorema 3.9 Si T = es una teorı́a de primer orden con igualdad que es consistente, entonces
T = tiene un modelo normal.
Demostración: Puesto que T = es consistente, debe tener un modelo M = (U, I). Puesto que
M satisface (E1 ), (E2 ) y (E3 ), se tiene que I(E) es una relación de equivalencia en U . Denotemos
por [u] la clase de equivalencia a la que pertenece d. Consideremos la interpretación (U/I(E), I ⋆ )
donde
1. I ⋆ (a) = [I(a)] para cada sı́mbolo de constante a.
2. I ⋆ (f )([u1 ], . . . , [un ]) = [I(f )(u1 , . . . , un )] para cada sı́mbolo de función n-aria f .
3. ([u1 ], . . . , [un ]) ∈ I ⋆ (P ) si y sólo si (u1 , . . . , un ) ∈ I(P ) para cada sı́mbolo de predicado
n-ario P .
El lector puede comprobar que esta interpretación es también un modelo para T = , y que en ella
I ⋆ (E) es la identidad en U/I(E); por lo tanto, es un modelo normal para T = .
En adelante usaremos = para E y 6= para ¬E.
En las teorı́as de primer orden con igualdad, podemos ampliar la potencia expresiva del len-
guaje: Hasta ahora disponı́amos del sı́mbolo de cuantificación ∀ para expresar que “todos” los
individuos de un dominio poseen cierta propiedad o están en una cierta relación y del sı́mbo-
lo de cuantificación ∃ para expresar que “al menos” un individuo de un dominio posee cierta
propiedad o está en una cierta relación. En una teorı́a de primer orden con igualdad podemos
expresar:
“existe exactamente 1 individuo que es P ” :
(∃x) P (x) ∧ (∀y)(P (y) → (y = x))
“hay al menos dos individuos tales que poseen la propiedad P ” :
(∃x)(∃y)(P (x) ∧ P (y) ∧ (x 6= y))
“existen exactamente 2 individuos que poseen la propiedad P ”
(∃x)(∃y) P (x) ∧ P (y) ∧ y 6= x ∧ (∀z)(P (z) → ((z = x) ∨ (z = y)))
“hay a lo sumo 2 individuos tales que P ”
(∀x)(∀y)(∀z) (P (x) ∧ P (y) ∧ P (z)) → ((x = y) ∨ (y = z) ∨ (x = z))
“hay al menos tres individuos tales que poseen la propiedad P ” :
(∃x)(∃y)(∃z)(P (x) ∧ P (y) ∧ P (z) ∧ (x 6= y) ∧ (x 6= z) ∧ (y 6= z))
Ası́ podemos seguir tanto como deseemos.
3.4. ALGUNAS TEORÍAS DE PRIMER ORDEN CON IGUALDAD 91
Orden parcial: Pretende describir todos los conjuntos parcialmente ordenados; por lo tanto,
su signatura satisface las siguientes propiedades:
1. (∀x)(x ≤ x)
2. (∀x)(∀y)((x ≤ y ∧ y ≤ x) → x = y)
3. (∀x)(∀y)(∀z)((x ≤ y ∧ y ≤ z) → x ≤ z)
Un sı́mbolo de función monaria: f11 (para “sucesor” ) y dos sı́mbolos de funciones binarias:
f12 (para “suma” ) y f22 (para “producto” ).
Denotamos por N al sistema de primer orden con igualdad que tiene como esquemas de axiomas
propios (E1 )–(E5 ) y además
A partir de (N7 ) y (MP) obtenemos la siguiente regla derivada, a la que se denomina regla de
inducción, (Ind):
A(a), (∀x)(A(x) → A(f11 (x))) ⊢ (∀x)A(x))
3.5. EJERCICIOS 93
Un sı́mbolo de constante: e.
Sus esquemas de axiomas propios son (E1 )–(E5 ) y los siguientes esquemas:
1. (∀x)(∀y)(∀z)[((x ∗ y) ∗ z) = (x ∗ (y ∗ z))]
2. (∀x)(e ∗ x = x)
3. (∀x)(∃y)(y ∗ x = e)
3.5. Ejercicios
1. Justificar las siguiente regla derivada (conocida como Regla Existencial ) para el sistema de Lukasiewicz:
Si t es libre para x en la fórmula A, entonces
A(t) ⊢ (∃x)A(x)
⊢ (∀x)(A → B) → (∃x)A → B)
a) x es el máximo .
b) x es maximal.
c) no existe ningún elemento entre x e y.
d ) x es el sucesor inmediato de y.
11. Probar en N :
a) 1 + 1 = 2
b) Probar que (∀x)(0 + x = x)
para destacar que si una caja está sobre algo, entonces está por encima de ese algo.
Elegimos una configuración de las cajas, a saber, a y c están sobre la mesa y b está sobre a. En
consecuencia, elegimos los tres axiomas siguientes:
(Ax3 ) S(a, m)
(Ax4 ) S(c, m)
(Ax5 ) S(b, a)
Usar esta teorı́a para razonar formalmente sobre el mundo que acabamos de describir. Concreta-
mente:
b) Extender la teorı́a para expresar que una caja está cerrada si tiene otra caja sobre ella, y
abierta en otro caso. Probar que b está abierta.
c) Extender la teorı́a para incluir la idea de que dos objetos están al mismo nivel si están sobre
el mismo objeto, y luego demostrar que a y c están al mismo nivel.
d) Extender la teorı́a de c) para incluir la idea de que dos cajas están al mismo nivel si los
objetos sobre los que se apoyan están al mismo nivel. Añadir dos nuevas cajas d y e, la caja
d sobre la mesa y e sobre d; después demostrar que b y e están al mismo nivel.
14. Considerar la siguiente teorı́a, denominada teorı́a de un acto vil [?], diseñada para representar un
mundo en el que se ha cometido un crimen. El escenario es el siguiente:
Sólo Tomás y Helenio tienen llaves. Alguien robó el dinero abriendo la caja fuerte. La
única forma de abrir la caja fuerte es con la llave.
La signatura consta de
Dos sı́mbolos de constantes: a para denotar Tomás y b para denotar Helenio.
Tres sı́mbolos de predicados:
a) R(x) para expresar x robó el dinero.
b) C(x) para expresar x abrı́a la caja fuerte.
c) Ll(x) para expresar x tenı́a una llave.
Los axiomas necesarios para formalizar la situación son
Usar esta teorı́a para razonar formalmente sobre el mundo que acabamos de describir. Concreta-
mente:
a) Probar que bien Helenio o bien Tomás robó dinero, es decir, ⊢ R(a) ∨ R(b).
b) Extender la teorı́a para incluir la afirmación de la inocencia de Tomás, y demostrar la culpa-
bilidad de Helenio.
96 CAPÍTULO 3. SISTEMAS DEDUCTIVOS PARA L1
Capı́tulo 4
En el capı́tulo anterior hemos introducido los sistemas de deducción para la lógica de primer orden, en
este tema y en el siguiente abordamos la posibilidad de automatización de las demostraciones en esta
nueva lógica.
Como hemos analizado en los Capı́tulos 2 y 3, para la lógica de primer orden, la demostración automática
de teoremas sólo puede aspirar a encontrar procedimientos de semidecisión, es decir, procedimientos que
aseguran su terminación sólo si la fórmula o inferencia a la que se aplican es válida. Como en el caso
proposicional, la mayor parte de los trabajos en este área se basan en dos métodos de refutación:
1. método de las tablas semánticas o de construcción de modelos.
2. método de resolución.
En este capı́tulo extendemos a la lógica de primer orden el primero de ellos.
Introducimos el método como extensión del expuesto para la lógica proposicional, ası́ pues, presentamos
la formulación del método debida a Jeffrey.
Como tal sistema de refutación, para verificar la validez de una fórmula A, el método de tablas semánticas
determina si ¬A es satisfacible. Para ello 1 el método organiza la búsqueda sistemática de un modelo
para A. Si la búsqueda tiene éxito, A no es válida, pero si la búsqueda fracasa, entonces A es válida.
Similarmente, si se trata de comprobar la validez de la inferencia de una fórmula A a partir de un conjunto
de hipótesis Γ, entonces el método determina la satisfacibilidad de Γ ∪ {¬A} buscando sistemáticamente
un modelo para dicho conjunto. Si la búsqueda tiene éxito, la inferencia es válida, en caso contrario, no
es válida.
Por lo tanto, tendremos que extender el método visto para el caso proposicional, de modo que incluya
una búsqueda de instanciaciones de fórmulas cuantificadas.
Definición 4.1 Dado el conjunto de fbfs Ω = {A1 , . . . , An } cuya satisfacibilidad se quiere comprobar, se
organizan las fórmulas de Ω en un árbol de una sola rama con razón A1 y tal que cada Ai con 2 ≤ i ≤ n
es sucesor inmediato de Ai−1 , es decir,
A1
A2
..
.
An
El árbol inicial asociado a Ω se irá ampliando sucesivamente mediante reglas de extensión basadas tan
sólo en la estructura sintáctica de las fbfs.
Para la descripción del método utilizaremos, como en el caso proposicional, la notación uniforme de
Smullyan, es decir, agruparemos las fórmulas no literales cuya conectiva principal es una conectiva boo-
leana en fbfs de tipo α (o de comportamiento conjuntivo) y de tipo β (o de comportamiento disyuntivo).
Las siguientes tablas muestran las fbfs de tipo α y las fbfs de tipo β junto con sus componentes.
α α1 α2
β β1 β2
A∧B A B
A∨B A B
¬(A ∨ B) ¬A ¬B
¬(A ∧ B) ¬A ¬B
¬(A → B) A ¬B
A→B ¬A B
¬¬A A A
Para clasificar las fbfs cuantificadas, introducimos dos nuevos tipos de fórmulas: fbfs de tipo δ (o
cuantificadas existencialmente) y fórmulas de tipo γ (o cuantificadas universalmente).
Las siguientes tablas muestran las fórmulas de tipo δ y de tipo γ junto con sus componentes.
δ δ(t) γ γ(t)
¬(∀x)A(x) ¬A(t) ¬(∃x)A(x) ¬A(t)
(∃x)A(x) A(t) (∀x)A(x) A(t)
(α) Si ρA denota la rama determinada por el nodo hoja A y una α-fórmula ocurre en ρA , extendemos
dicha rama añadiendo:
(a) Dos nodos etiquetados con sus componentes α1 , α2 si α1 6= α2 .
(b) Un nodo etiquetado con la componente común si α1 = α2 .
y marcamos la α-fórmula como ya usada:
.. ..
. .
α α X
−→
.. ..
. .
A A
α1
α2
(β) Si ρA denota la rama determinada por el nodo hoja A y una β-fórmula ocurre en ρA , extendemos
dicha rama añadiendo:
2
Las reglas (α) y (β) son las mismas que en el caso proposicional
99
(a) Dos nodos (como descendiente izquierdo y derecho) etiquetados con sus componentes β1 y β2
respectivamente, si β1 6= β2 .
(b) Un nodo etiquetado con la componente común , si β1 = β2 .
y marcamos la β−fórmula
.. como ya usada: ..
. .
β β X
.. ..
. −→ .
A A
@
@
β1 β2
Las reglas (δ) y (γ) requieren considerar, como hicimos en la Definición 1.42 sobre skolemización y por
idénticos motivos, la extensión de L1 :
Definición 4.2 Dado un lenguaje L1 de primer orden, definimos L+ 1 como la extensión de L1 obtenida
añadiendo a su alfabeto un conjunto infinito numerable C ′ de nuevos sı́mbolos de constante a los que
llamaremos parámetros.
(δ) Si ρA denota la rama determinada por el nodo hoja A y una fórmula δ(x) ocurre en ρA , extendemos
dicha rama añadiendo δ(a), donde a es un parámetro que no aparece previamente en la rama, y
marcamos la δ-fórmula:
.. ..
. .
δ(x) δ(x) X
.. −→ ..
. .
A A
δ(a)
(γ) Si ρA denota la rama determinada por el nodo hoja A y una fórmula γ(x) ocurre en ρA , extendemos
dicha rama añadiendo γ(t) donde t es un término básico que aparece previamente en la rama.
.. ..
. .
γ(x) γ(x)
.. −→ ..
. .
A A
γ(t)
ee
rr
La definición de las reglas γ y δ corroboran la idea de que las γ-fórmulas son de tipo universal
y la δ-fórmulas son de tipo existencial.
Conviene resaltar que la regla δ (para fbfs de carácter existencial) permite eliminar la cuan-
tificación sustituyendo la variable cuantificada por un nuevo sı́mbolo de constante (concre-
tamente, un parámetro) y marcando como usada la fbf δ(x). Por el contrario, una aplicación
de la regla γ (para fbfs de carácter universal) permite sustituir la variable cuantificada por
100 CAPÍTULO 4. MÉTODO DE LAS TABLAS SEMÁNTICAS
un término que apareció anteriormente (es decir, sobre el que ya estamos interesado) pero
no estará permitido marcar la fbf γ(x).
La regla γ es, por lo tanto, la única que no sustituye la fbf por otras más simples: añade
una más simple pero mantiene la de partida. La razón es que, claramente, con [x/t]A(x)
no cubrimos toda la información contenida en (∀x)A(x); puede ser necesario en una etapa
posterior instanciar (∀x)A(x) con algún otro término t′ y expandir la rama con A(t′ ). De
esta forma aseguramos que las fbfs cuantificadas universalmente se podrán instanciar con
términos básicos que aún no han sido introducidos.
Definición 4.3 Sea Ω = {A1 , . . . , A2 } un conjunto de fbfs. Un árbol T se dice que es un árbol para Ω,
si existe una secuencia de árboles T1 , . . . , Tn tal que:
T1 es el árbol inicial asociado a Ω, es decir, el árbol de una sola rama:
A1
A2
..
.
An
ee
rr
En adelante, en los ejemplos, añadiremos un subı́ndice a las marcas X, que nos indique el
orden de aplicación de las reglas.
Ejemplo 4.1 Si no exigimos que cada aplicación de la regla δ introduzca una nueva constante, podrı́amos
cometer el error de concluir que la fórmula
es válida:
¬[(∀x)(P (x) ∨ Q(x)) → ((∀x)P (x) ∨ (∀x)Q(x))] X1
(∀x)(P (x) ∨ Q(x)) X5 [x/a])
¬((∀x)P (x) ∨ (∀x)Q(x)) X2
¬(∀x)P (x) X3 [x/a]
¬(∀x)Q(x) X4 [x/a] (Hemos utilizado de nuevo a)
¬P (a)
¬Q(a)
P (a) ∨ Q(a) X6
@
@
P (a) Q(a)
× ×
101
no es un modelo para A.
Ejemplo 4.2 Aún aplicando correctamente la regla δ, si se aplica la regla γ marcamos la fórmula,
podrı́amos cometer el error de concluir que dada la fórmula
La imposibilidad de marcar una γ-fórmula una vez que ha sido usada plantea varios problemas: ¿Cómo
se define el concepto de rama completa? Este concepto es necesario para describir el método, puesto que
si se extiende directamente la definición proposicional, olvidando el tratamiento especial necesario para
las γ-fórmulas, no es posible demostrar que toda rama abierta de un árbol completo es satisfacible. La
solución a este problema pasa por definir un método sistemático de búsqueda.
Si el árbol obtenido en el n-ésimo paso es un árbol cerrado, el método termina con salida es
VÁLIDA
Si el árbol obtenido en el n-ésimo paso es tal que para cada rama abierta toda fórmula no atómica
ha sido marcada, entonces el método termina con salida NO es VÁLIDA.
En otro caso, consideramos un nodo A de profundidad minimal que aún no haya sido usado y que
aparezca en alguna rama abierta. La extensión de la tabla se realiza para cada rama abierta ρX
(con nodo hoja etiquetado con X) como se indica a continuación:
1. Si A es del tipo α la rama ρX se extiende añadiendo α1 y α2 .
102 CAPÍTULO 4. MÉTODO DE LAS TABLAS SEMÁNTICAS
2. Si A es del tipo β la rama ρX se bifurca en dos ramas añadiendo dos nodos etiquetados con
β1 y β2 respectivamente.
3. Si A es del tipo δ la rama ρX se extiende marcando A y añadiendo un nodo δ(a), donde a es
un parámetro que no aparece previamente en la rama.
4. Finalmente, y este es el caso delicado, si A es del tipo γ se marca A y se extiende la rama
añadiendo dos nodos etiquetados con γ(t) y A respectivamente, donde t es un término básico
que aparece previamente en ρX (o un parámetro arbitrario, si no existe tal término).
ee
rr
Nótese que para conservar la universalidad de las γ-fórmulas se repite el nodo γ, pero a
mayor profundidad; esto permite usar todas las γ-fórmulas que aparezcan de modo rotativo
y permite marcar el nodo como usado.
Definición 4.5 Una rama abierta ρ de un árbol T para Ω se dice completa si satisface las siguientes
condiciones:
1. Si una fórmula α ocurre en la rama ρ, también sus componentes α1 y α2 ocurren en ρ.
2. Si una fórmula β ocurre en la rama ρ, o la componente β1 o la componente β2 ocurre en ρ.
3. Si una fórmula δ ocurre en la rama ρ, una componente δ(a) ocurre en ρ para algún parámetro a.
4. Si una fórmula γ ocurre en la rama ρ, las componentes γ(t) ocurren en ρ para todo término básico.
Un árbol T para Ω se dice terminado si toda rama es cerrada o completa.
Definición 4.6 Llamaremos refutación para un conjunto Ω de fbfs a cualquier árbol cerrado para Ω. Una
fórmula C se dice que se deriva o infiere del conjunto de fórmulas {H1 , . . . , Hn }, si existe una refutación
para {H1 , . . . , Hn , ¬C}. En particular, una fórmula A se dice demostrable si existe una refutación para
{¬A}.
Una rama ρ se dice satisfacible si el conjunto de las fbfs que etiquetan los nodos ρ es satisfacible. Un
árbol T para Ω se dice satisfacible si alguna de sus ramas es satisfacible.
SI NO
ES VÁLIDA
SI NO
NO ES VÁLIDA
2. Tal y como se refleja en el diagrama, el orden de prioridad de las extensiones es α, γ y β. Este orden
está determinado por cuestiones de eficiencia; dejamos para el final la extensión β, responsable de
la generación de nuevas ramas.
3. Las extensiones δ se hacen cuando no haya fórmulas α, γ o β sin marcar: se elige una fórmula δ,
se aplica la δ regla y se vuelve a aplicar la regla γ con la nueva constante introducida.
4. El orden de expansión de las fórmulas y de los términos usados en las extensiones γ no condiciona
la corrección del método, pero sı́ el tamaño de la tabla construida. En las implementaciones del
algoritmo es necesario establecer un orden, pero en la aplicación manual podremos elegir libremente
las fórmulas y términos, aunque respetando siempre los criterios de prioridad.
Demostración: Puesto que, por construcción, nunca realizamos extensiones sobre una rama cerrada,
tenemos asegurado que toda rama cerrada es finita. Por lo tanto, el lema de König asegura el resultado.
Teorema 4.2 Si T es un árbol satisfacible para Ω entonces todo árbol para Ω obtenido al aplicar a T
cualquier regla de extensión es también satisfacible.
Demostración: Sea T un árbol satisfacible para Ω y sea ρ una rama satisfacible de T . Supongamos que
T ′ ha sido obtenido al aplicar una regla de extensión a un nodo de la rama ρ′ de T que está etiquetado
con una fbf A. Entonces,
4.2. CORRECCIÓN Y COMPLETITUD 105
Teorema 4.3 (Existencia de modelo) Toda rama completa y abierta ρ de un árbol T para un conjunto
de fbfs Ω es satisfacible.
Por tanto, A tiene que ser una α, una β, una δ o una γ. Veamos que tampoco puede darse ninguno de
estos casos.
Si A fuera una α, dado que ρ es una rama completa y abierta se tiene que α1 y α2 ∈ F BF ρ . Como
gr(α1 ), gr(α2 ) < gr(α), entonces por la hipótesis (H), I ρ (α1 ) = I ρ (α1 ) = 1. Entonces I ρ (α) = 1. Pero
esto contradice (H), que establece que I ρ (A) = I ρ (α) = 0. Ası́ pues, A no puede ser una α.
Si A fuera una β, dado que ρ es una rama completa y abierta se tiene que β1 ∈ F BF ρ o bien β2 ∈ F BF ρ .
Dado que gr(β1 ), gr(β2 ) < gr(β), por (H) tendrı́amos que si β1 ∈ F BF ρ , entonces I ρ (β1 ) = 1 y si
106 CAPÍTULO 4. MÉTODO DE LAS TABLAS SEMÁNTICAS
β2 ∈ F BF ρ , entonces I ρ (β2 ) = 1. En cualquier caso, I ρ (β) = 1. Pero esto contradice la hipótesis (H), la
cual establece que I ρ (A) = I ρ (β) = 0. Ası́ pues, A tampoco puede ser una β.
Si A fuera una δ, dado que ρ es una rama completa y abierta se tiene que δ(a) ∈ F BF ρ , para alguna
constante a. Dado que gr(δ(a)) < gr(δ), por la hipótesis (H) resulta que I ρ (δ(a)) = 1. Entonces I ρ (δ) = 1.
Pero esto contradice (H), que establece que I ρ (A) = I ρ (δ) = 0.
Si A fuera una γ, dado que ρ es una rama completa y abierta se tiene que γ(t) ∈ F BF ρ , para todo
término t ∈ T ermbρ . Dado que gr(γ(t)) < gr(γ) para todo t ∈ T ermbρ , por la hipótesis (H) resulta que
I ρ (γ(t)) = 1 para todo t ∈ T ermbρ . Entonces I ρ (γ) = 1. Pero esto contradice (H), que establece que
I ρ (A) = I ρ (γ) = 0.
Hemos recorrido las posibles formas de A y en ningún caso puede ser I ρ (A) = 0. Por tanto, toda fórmula
de F BF ρ es verdadera en Mρ . De esto se sigue que ρ tiene un modelo y, por tanto, el árbol tiene una
rama satisfacible. Esto concluye la prueba.
Demostración:
1. Suponemos que existe una refutación para {H1 , . . . , Hn , ¬C}. Deseamos probar H1 , . . . , Hn |= C,
es decir que {H1 , . . . , Hn , ¬C} es insatisfacible. Lo probamos por reducción al absurdo:
Si Ω = {H1 , . . . , Hn , ¬C} fuera satisfacible, por el Teorema 4.2, todo árbol asociado a Ω es satis-
facible, es decir, todo árbol para Ω tendrı́a una rama abierta, lo cual es imposible por hipótesis.
2. Suponemos H1 , . . . , Hn |= C. Deseamos probar que existe una refutación para {H1 , . . . , Hn , ¬C}.
Lo probamos por reducción al absurdo:
Si no existiera una refutación para Ω = {H1 , . . . , Hn , ¬C}, y si T es un árbol asociado a Ω, T tiene
una rama abierta ρ tal que tras la aplicación de reglas a sus nodos sigue proporcionando una rama
abierta. Ahora bien, la construcción sistemática, nos asegura que para todo nodo N en ρ si A es
la etiqueta de N y A no está marcada, el método aplicará en algún momento de su ejecución una
regla a A.
En particular, si A es una γ-fórmula y t es un término básico que ocurre en ρ, existe un descendiente
N ′ de N etiquetado con γ(t). En definitiva, construirı́amos una rama abierta y completa y, por
el Teorema 4.3 de existencia de modelo, Ω = {H1 , . . . , Hn , ¬C} serı́a satisfacible en contra de la
hipótesis.
Para acercarnos intuitivamente a la búsqueda de modelos, veamos el siguiente ejemplo resuelto a nivel
semántico.
Ejemplo 4.4 Vamos a buscar un modelo de la fórmula
Más formalmente, el teorema de existencia de modelos, Teorema 4.3, asegura que en un árbol terminado
para un conjunto Ω de fbfs, cada rama abierta ρ, proporciona un modelo para Ω, concretamente, el
modelo de Herbrand respecto de L+ 1 determinado por la interpretación I tal que I(A) = 1 si A ocurre en
ρ e I(A) = 0 si ¬A ocurre en ρ.
Ejemplo 4.5 La fórmula A = (∃x)(∀y)R(x, y) → (∃x)R(x, a) es válida.
Ejemplo 4.6 La fórmula A = (∀x)(P (x) → Q(x)) → ((∀x)P (x) → (∀x)Q(x)) es válida.
donde cada rama abierta nos proporciona un modelo para la fórmula ¬A.
En este ejemplo, para hacer más simple el gráfico, en lugar de marcar las γ-fórmulas y repetirlas tras
su uso, hemos indicado a su derecha el orden en que han sido utilizadas, detallando las sustituciones
4.2. CORRECCIÓN Y COMPLETITUD 109
realizadas.
(∀x)(∃y)P (y, x) ((2)[x/a]; (8)[x/b])
(∀u)(∀v)(P (u, v) → Q(u, v)) ((3)[u/a]; (9)[u/b])
¬(∀z)(∃t)Q(t, z) X1
¬(∃t)Q(t, a) ((4)[t/a]; (10)[t/b])
((∃y)P (y, a) X7
(∀v)(P (a, v) → Q(a, v)) ((5)[v/a]; (11)[v/b])
¬Q(a, a)
P (a, a) → Q(a, a) X6
@@
¬P (a, a) Q(a, a)
×
P (b, a)
(∃y)P (y, b)
(∀v)(P (b, v) → Q(b, v)) ((12)[v/a]; (13)[v/b])
¬Q(b, a)
P (a, b) → Q(a, b) X14
P (b, a) → Q(b, a) X15
P (b, b) → Q(b, b)
@
@
¬P (a, b) Q(a, b)
@@ @@
¬P (b, a) Q(b, a) ¬P (b, a) Q(b, a)
× × × ×
Ejemplo 4.9 Vamos a estudiar la validez del siguiente razonamiento usando el método de Gilmore y el
de las Tablas semánticas.
El padre del padre de una persona es su abuelo, toda persona tiene un padre; por lo tanto
todo el mundo tiene un abuelo.
Leyendo la relación P (x, y) como “x es padre de y” y la relación A(x, y) como “x es abuelo de y” podemos
escribir la siguiente formalización:
{(∀x)(∀y)(∀z)((P (x, y) ∧ P (y, z)) → A(x, z)), (∀x)P (f (x), x), ∀y¬A(y, a)}
Su dominio de Herbrand es
HS = {a, f (a), f (f (a)), f (f (f (a))), . . . }
y la base de Herbrand
BS = {P (t1 , t2 ); t1 , t2 ∈ HS } ∪ {A(t1 , t2 ); t1 , t2 ∈ HS }
La tabla semántica que demuestra igualmente la validez del razonamiento se muestra a continuación. La
diferencia de tamaño entre los dos árboles no debe conducir a conclusiones erróneas sobre la complejidad
de los métodos. Debe tenerse en cuenta que, por una parte, el método de Gilmore requiere un proceso de
normalización previo y que, además, en ambos casos hemos elegido un orden óptimo para las sucesivas
extensiones de los árboles.
Es interesante comparar las dos soluciones. En las dos, hemos necesitado tres elementos para lograr las
inconsistencias: a, b y c en las tablas y a, f (a) y f (f (a)) en el árbol de Gilmore. Además, en ambos casos,
el significado de los mismos en el modelo es el mismo: b es el padre de a y c es el padre de b, ası́ como
f (a) es el padre de a y f (f (a)) es el padre de f (a).
4.3. EJERCICIOS 111
4.3. Ejercicios
1. Aplicar el método de las tablas semánticas para analizar la validez o no de las siguientes fbfs:
a) (∃x)((∃yP (y) → P (x))
b) (∀x)(∃y)P (x, y) → (∃z)(∀t)P (t, z)
c) (∃x)(P (x) → Q(x)) → ((∃xP (x) → (∃x)Q(x))
d ) (∀x)(P (x) → Q(x)) → ((∀x)P (x) → (∀x)Q(x))
e) (∀x)[P (x) → (∃y)(Q(y) ∧ R(y, x))] ↔ (∃x)[Q(x) ∧ (∀y)(P (y) → R(x, y))]
f ) (∀x)(P (x) ∧ Q(x)) → ((∀x)P (x) ∧ (∀x)Q(x))
g) ((∀x)P (x) ∧ (∀x)Q(x)) → (∀x)(P (x) ∧ Q(x))
2. Aplicar el método de las tablas semánticas para analizar la validez o no de las siguientes fbfs:
a) (∀x)(P (x) ∨ Q(x)) → ((∀x)P (x) ∨ (∀x)Q(x))
b) ((∀x)P (x) → (∀x)Q(x)) → (∀x)(P (x) → Q(x))
c) (∃x)(∀y)R(x, y) → (∀y)(∃x)R(x, y)
d ) (∃x)(P (x) → (∀x)P (x))
e) (∀x)(∀y)(P (x) ∧ P (y)) → (∃x)(∃y)(P (x) ∨ P (y))
f ) (∀x)(∀y)(P (x) ∧ P (y)) → (∀x)(∀y)(P (x) ∨ P (y))
g) (∀x)(∃y)(∀z)(∃w)(R(x, y) ∨ R(w, z))
3. Aplicar el método de las tablas semánticas para analizar la validez o no de la siguiente inferencia
(∀x)(∃y)P (x, y)
(∀x)¬P (x, x)
(∃x)(∃y)(∃z)¬ (P (x, y) ∧ P (y, z)) → P (x, z)
(∃x)(∀y)P (x, y)
(∃x)(∃y)(P (x, y) → Q(x, y))
(∃x)(∀y)Q(x, y)
6. Aplicar el método de las tablas semánticas para analizar la validez o no del siguiente razonamiento:
7. Tras skolemizar, probar usando el método de las tablas semánticas para probar la satisfacibilidad
o no de los siguientes conjuntos de fbfs
112 CAPÍTULO 4. MÉTODO DE LAS TABLAS SEMÁNTICAS
9. Aplique el método de las tablas semánticas para analizar la validez del razonamiento siguiente:
El padre del padre de una persona es su abuelo, toda persona tiene un padre; por lo
tanto todo el mundo tiene un abuelo.
10. Aplique el método de las tablas semánticas para analizar la validez o no del razonamiento siguiente:
Ningún vendedor de coches usados compra un coche usado para uso familiar.
Algunos de los que compran un coche usado para uso familiar son deshonestos.
11. Aplicar el método de las tablas semánticas para analizar la validez o no de los siguientes razona-
mientos:
a) Todo estudiante es honesto, Juan no es honesto; por lo tanto Juan no es estudiante.
b) Todo atleta es fuerte, todo el que es fuerte e inteligente triunfará en su carrera, Pedro es un
atleta, Pedro es inteligente; por lo tanto Pedro triunfará en su carrera.
c) Todo aquel que ama a alguien ama a Dios, no hay nadie que no ame a nadie; por lo tanto
todo el mundo ama a Dios.
d ) El padre del padre de una persona es su abuelo, toda persona tiene un padre; por lo tanto
todo el mundo tiene un abuelo.
12. Estudie la validez de la siguientes inferencias utilizando Tablas semánticas:
(∀x)(C(x) → (W (x) ∧ R(x)))
a) (∃x)(C(x) ∧ O(x))
(∃x)(O(x) ∧ R(x))
(∀y)(S(y) → C(y))
b)
(∀x)((∃y)(S(y) ∧ V (x, y)) → (∃z)(C(z) ∧ V (x, z)))
¬(∀x)(F (x) → (∀y)(G(y) → H(x)))
c) (∃x)F (x) ∧ (∃x)¬(F (x) ∨ G(x))
(∀x)(F (x) → H(x))
(∀x)(G(x) ∨ (∃y)H(y))
d) ¬(∃x)G(x)
¬(∃x)¬H(x)
(∀x)(F (x) → G(x))
e) ¬(∃x)(F (x) ∧ G(x))
¬(∃x)F (x)
(∀x)(H(x) → A(x))
f)
(∀x)((∃y)(H(y) ∧ T (x, y)) → (∃y)(A(y) ∧ T (x, y)))
4.3. EJERCICIOS 113
(∃x)(F (x) ∧ ¬G(x))
(∀x)(F (x) → H(x))
g) (∀x)(J(x) ∧ (K(x) → F (x)))
(∃x)(H(x) ∧ ¬G(x)) → (∀x)(K(x) → ¬H(x))
(∀x)(J(x) → ¬K(x))
F (a)
h)
(∀x)(F (x) → G(x)) ↔ (∀x)((F (x) ∧ G(x)) ∨ (¬F (x) ∧ G(a)))
(∀x)(∃y)P (x, y)
i) (∀x)¬P (x, x)
(∃x)(∃y)(∃z)¬((P (x, y) ∧ P (y, z)) → P (x, z))
(∃x)(∀y)P (x, y)
j) (∃x)(∃y)(P (x, y) → Q(x, y))
(∃x)(∀y)Q(x, y)
114 CAPÍTULO 4. MÉTODO DE LAS TABLAS SEMÁNTICAS
Capı́tulo 5
Método de Resolución
115
116 CAPÍTULO 5. MÉTODO DE RESOLUCIÓN
En definitiva, no podemos olvidar que la forma clausal Ω = {P (f (x)))} representa la fbf (∀)P (f (x) y, en
general,
Si C una cláusula y {x1 , . . . , xn } es el conjunto de variables que interviene en C
entonces: Una interpretación M es un modelo para C si y sólo si M es un modelo
para (∀x1 ) . . . (∀xn )C(x1 , . . . , xn ).
¿Disponemos de algún resultado especı́fico sobre la satisfacibilidad de un conjunto infinito de cláusulas
básicas? Afortunadamente sı́: disponemos del teorema de Compacidad de Herbrand, que nos asegura
que: si Ω es un conjunto de cláusulas y Ωb el conjunto de instancias básicas de Ω, entonces
Ası́ que podemos empezar planteándonos la primera extensión obvia del método para analizar la satisfa-
cibilidad de un conjunto de cláusulas básicas.
C1
C2
RA (C1 , C2 )
Ejemplo 5.1
1. RP (a) (¬P (a) ∨ Q(a, b) ∨ ¬R(f (c)), P (a) ∨ Q(a, b) ∨ S(b, g(d, e))) = Q(a, b) ∨ ¬R(f (c)) ∨ S(b, g(d, e))
2. RQ(a,b) (¬P (a) ∨ Q(a, b) ∨ ¬R(f (c)), P (a) ∨ ¬Q(a, b) ∨ S(b, g(d, e))) =
¬P (a) ∨ ¬R(f (c)) ∨ P (a) ∨ S(b, g(d, e))
3. RP (a) (P (a), ¬P (a)) = 2
4. RR(f (c)) (Q(a, b) ∨ R(f (c)), ¬P (a) ∨ ¬R(f (c))) = Q(a, b) ∨ ¬P (a)
5. RP (a) (Q(a, b) ∨ R(f (c)), ¬P (a) ∨ ¬R(f (c))) No existe
5.1. RESOLUCIÓN BÁSICA 117
La justificación semántica de la regla de resolución para cláusulas básicas es la misma que en el caso
proposicional 1 y, como consecuencia trivial, se tiene:
Teorema 5.1 (Corrección del principio de resolución) Dado un conjunto de cláusulas básicas Ω,
si C1 , C2 ∈ Ω son resolubles entonces
Definición 5.2 Dado un conjunto de Ω de cláusulas básicas y una cláusula básica C, se dice que C es
deducible por resolución a partir de Ω, denotado Ω ⊢R C, si existe una secuencia de cláusulas básicas
C1 , C2 , · · · , Cn tal que
1. Cada Ci (1 ≤ i ≤ n) es o bien una cláusula de Ω o bien una resolvente de dos cláusulas anteriores
en la secuencia.
2. Cn = C.
La secuencia Ci (1 ≤ i ≤ n) se dice que es una deducción por resolución de C a partir de Ω.
A una deducción por resolución de 2 a partir de Ω se le denomina una refutación por resolución de
Ω.
Ejemplo 5.2 Demos una refutación por resolución del siguiente conjunto finito de cláusulas básicas:
Ω = {P (a) ∨ Q(a, b), ¬Q(a, b) ∨ R(f (c)), ¬P (a) ∨ R(f (c)), ¬R(f (c))}
El modo habitual de representar las deducciones por resolución a partir de un conjunto Ω de cláusulas
es mediante un árbol binario, llamado árbol de resolución:
Definición 5.3 Un árbol de resolución para un conjunto de cláusulas básicas Ω es un árbol caracte-
rizado como sigue:
1. cada nodo no hoja tiene dos descendientes inmediatos.
2. cada nodo hoja está etiquetado por una cláusula de Ω.
3. cada nodo no hoja está etiquetado por una resolvente de las etiquetas de sus descendientes inme-
diatos.
A ∨ B, ¬A ∨ C |= B ∨ C
118 CAPÍTULO 5. MÉTODO DE RESOLUCIÓN
P (a) ∨ Q(a, b) ¬P (a) ∨ R(f (c)) ¬R(f (c)) ¬Q(a, b) ∨ R(f (c)) ¬R(f (c))
@ @ @
@ @ @
@ @ @
¬P (a) ¬Q(a, b)
@
@
Q(a, b)@
@
@
@
@
@@
2
En general, para todo conjunto insatisfacible de cláusulas, Ω, existen refutaciones distintas para Ω. El
siguiente árbol muestra una nueva refutación para el conjunto de cláusulas del ejemplo anterior
¬P (a) ∨ R(f (c)) ¬R(f (c)) P (a) ∨ Q(a, b) ¬Q(a, b) ∨ R(f (c)) ¬R(f (c))
@
@
¬P (a)@
@
@
Q(a, b) @
@
@
R(f (c)) @
@
@@
2
Los ejemplos que hemos visto muestran la extensión del método de resolución para el caso de un conjunto
finito de cláusulas Ω y, como era de esperar, tal extensión es inmediata ¿Pero como operar en el caso de
un conjunto infinito de cláusulas Ω? Desearı́amos disponer de herramientas que nos permitan eludir la
ingente tarea de ir generando todos los subconjuntos finitos de Ωb . 2 Éste fue el objetivo de Robinson al
definir el método de resolución para L1 y a describirlo dedicamos el resto del capı́tulo.
Volvamos a nuestro problema, analizar la satisfacibilidad de un conjunto de cláusulas en L1 :
No tendremos problema para asegurar que Ω1 = {P (a), ¬P (a)} es insatisfacible ¿Pero que decimos del
conjunto Ω2 = {P (x), ¬P (y)}? Según lo que venimos analizando, Ω2 es satisfacible si y solo si Ωb2 es
satisfacible. Pero
P (a)
(∀x)(P (x) → P (f (x)))
(∀x)P (x)
1. P (a) de Ωb
2. ¬P (b) de Ωb
3. ¬P (a) ∨ P (f (a)) de Ωb
4. P (f (a)) RP (a) (1, 3)
5. ¬P (f (a)) ∨ P (f 2 (a)) de Ωb
6. P (f 2 (a)) RP (f (a)) (4, 5)
7. ... ...
...
Se puede generar la cláusula P (f n (a)) para todo n ∈ N∗ , pero ninguna otra cláusula. Por tanto el conjunto
de cláusulas es satisfacible.
En el ejemplo anterior, la simplicidad de Ωb nos ha permitido concluir la satisfacibilidad pero, desafor-
tunadamente, no existe un método general y eficiente para generar todas las instancias básicas de un
conjunto de cláusulas de L1 . Como hemos indicado, la idea de Robinson consiste en trabajar directamen-
te con las cláusulas sin tener que manejar explı́citamente las instancias básicas. Profundizamos ahora en
esta idea:
Si Ω consta de un par de cláusulas de L1 , por ejemplo, Ω = {P (x) ∨ Q(x), ¬P (f (y)) ∨ R(x, x)}, se tiene
que estas dos cláusulas
C1 = P (x) ∨ Q(x)
C2 = ¬P (f (y)) ∨ R(x, z)
no son resolubles en el sentido anterior (no contiene un literal y su negado), pero si consideramos las
siguientes instancias básicas de C1 y C2 :
éstas sı́ son resolubles y nos proporcionan como resolvente la cláusula Q(f (a)) ∨ R(f (a), z). Por lo tanto,
tendremos que modificar la definición de cláusulas resolubles de modo que podamos asegurar que dos
cláusulas C1 y C2 son resolubles si y sólo si existe una cláusula C1′ , instancia de C1 , y una cláusula C2′ ,
instancia de C2 , tales que C1′ y C2′ son resolubles. La idea de Robinson de trabajar directamente con
cláusulas con variables requiere considerar un mecanismo, debido a Herbrand, llamado “unificación”. Los
siguientes ejemplos nos ayudarán a comprender de qué se trata.
En el ejemplo anterior, hemos usado instancias básicas C1′ y C2′ . Ahora bien, puesto que al considerar
instancias de las cláusulas se ha podido llegar a un par resoluble, serı́a conveniente obtener la resolvente
120 CAPÍTULO 5. MÉTODO DE RESOLUCIÓN
más general posible, ası́ podrı́amos permitir que alguna de sus instancias se pueda resolver posteriormente
con alguna otra cláusula de Ω. Un ligero análisis permite encontrar una sustitución más general, [x/f (y)],
que también proporciona un par resoluble de cláusulas C1′ y C2′ :
las instancias obtenidas al realizar las sustituciones [x/f (b)], [y/a], [u/b], [v/a] y [w/a] se obtienen las
instancias básicas C1b , C2b y C3b :
C1b = P (f (b), a, a)
C2b = ¬P (f (b), a, a) ∨ Q(a, g(a, f (b))
C3b = ¬Q(z, g(a, f (b)))
En primer lugar, podemos ahora resolver C1b y C2b obteniendo Q(a, g(a, f (b))). Si ahora consideramos
la instancia obtenida al realizar la sustitución en la tercera cláusula [z/a], es decir, ¬Q(a, g(a, f (b))) la
resolvente de esta cláusula con Q(a, g(a, f (b))) es la cláusula vacı́a.
En general, todas las instancias con las sustituciones [x/f (t1 )], [y/t2 ], [u/t1 ], [v/a], [w/t2 ] y [z/a] donde
t1 , t2 ∈ HΩ nos permitirı́an generar rápidamente la cláusula vacı́a.
En el desarrollo de los ejemplos anteriores se han usado explı́citamente dos conceptos de interés: “sus-
titución” y “resolvente más general”. Implı́citamente, se ha usado el concepto de unificación debido a
Herbrand y que, como hemos indicado, es una herramienta fundamental en la extensión del método de
resolución al caso general. Pasamos ya a introducir estos conceptos.
5.2. Unificación
La unificación ha adquirido mucha significación en el contexto de las Ciencias de la Computación debido
a su gran espectro de aplicaciones; entre éstas encontramos el estudio de bases de datos, procesamiento
del lenguaje natural, sistemas expertos, lenguajes de manipulación de textos, sistemas de planificación,
sistemas de representación del conocimiento, lenguajes de programación lógica, sistemas de reescritura y
el álgebra computacional.
Comenzamos introduciendo la noción de sustitución (finita),4 si no hay lugar a confusión simplemente
diremos sustitución:
Definición 5.4 Sea Term el conjunto de términos de L1 . Una sustitución finita es una aplicación
θ : V → T erm que coincide con la aplicación identidad salvo en un número finito de variables, es decir,
tal que θ(x) = x salvo para un número finito de elementos x de V.
Si no hay lugar a confusión, nos referiremos a una sustitución finita σ simplemente como sustitución y
6 xi :
la representaremos mediante el conjunto de variables xi tal que σ(xi ) =
Dada una sustitución θ, la extendemos a Term del siguiente modo: θ(t) es el término obtenido sustituyendo
en t cada variable x por θ(x).
La aplicación de la sustitución θ a un término t se denotará por θt, y el término obtenido se dirá que es
una instancia de t. En particular, si θ es una sustitución básica, diremos que θt es una instancia básica
de t.
Si θ1 y θ2 son dos sustituciones, la composición de θ1 y θ2 , se denotará como θ2 ◦ θ1 . La operación ◦ es
asociativa y tiene como elemento unidad a la sustitución vacı́a ǫ.
Dadas dos sustituciones θ1 y θ2 definidas por
{x1 /θ2 (t1 ), . . . , xn /θ2 (tn ), yi1 /θ2 (yi1 ), . . . , yim /θ2 (yim )}
Ejemplo 5.6
1. Si θ1 = {x/y} y θ2 = {y/a} entonces θ2 ◦ θ1 = {x/a, y/a}.
2. Si θ1 = {y/f (x), z/b} y θ2 = {x/a} entonces θ2 ◦ θ1 = {x/a, y/f (a), z/b}.
3. Si θ1 = {x/y, y/f (b), z/b} y θ2 = {y/x} entonces θ2 ◦ θ1 = {y/f (b), z/b}.
4. Si θ1 = {x/y, y/f (b), z/b} y θ2 = {x/a} entonces θ2 ◦ θ1 = {x/y, y/f (b), z/b}.
La extensión de una sustitución finita al conjunto Atom de los átomos de L1 se realiza de forma obvia:
se tiene:
1. θ1 P (x, y, z, u)) = P (f (y), a, v, u)
2. θ2 ◦ θ1 P (x, y, z, u) = θ2 P (f (y), a, v, u)) = P (f (y), a, f (g(a)), u)
Definición 5.5 Diremos que un conjunto de términos {t1 , . . . , tn } es unificable si existe una sustitución
θ tal que θt1 = θt2 = . . . = θtn . Asimismo, diremos que un conjunto de átomos con el mismo predica-
do, {P (t11 , . . . , t1n ), . . . , P (tn1 , . . . , tm i i
n )}, es unificable si existe una sustitución θ tal que θP (t1 , . . . , tn ) =
j j
θP (t1 , . . . , tn ) para cualesquiera i y j tales que i, j ∈ {1, . . . , m}. En ambos casos diremos que θ es un uni-
ficador, del conjunto {t1 , . . . , tn } en el caso de términos, o del conjunto {P (t11 , . . . , t1n ), . . . , P (tm m
1 , . . . , tn )}
en el caso de unificación de átomos.
122 CAPÍTULO 5. MÉTODO DE RESOLUCIÓN
Ejemplo 5.8
1. Los átomos P (f (x), a) y P (y, f (w)) no son unificables ya que y y f (x) son unificables pero a y
f (w) no lo son.
2. Los átomos P (f (x), z) y P (y, a) son unificables y θ = {x/a, y/f (a), z/a} es un unificador. En efecto
θ(P (f (x), z)) = θ(P (y, a)) = P (f (a), a)
Definición 5.6 Dado un conjunto de términos {t1 , . . . , tn }, diremos que un unificador θ de {t1 , . . . , tn }
es de máxima generalidad (denotado umg) si para cualquier otro unificador σ de {t1 , . . . , tn } se tiene
que σ = λ ◦ θ para alguna sustitución λ.
Intuitivamente, un unificador de máxima generalidad realiza el menor número de sustituciones y las más
generales posibles, es decir, mantiene el mayor número posible de variables.
Ejemplo 5.9 Las sustituciones
θ1 = {x/a, z/f (a, a), y/u, v/b} y θ2 = {v/b, y/u, z/f (a, x)}
son unificadores del conjunto de términos {h(f (a, x), f (y, b)), h(z, f (u, v))}.
En efecto,
θ1 (h(f (a, x), f (y, b))) = θ1 (h(z, f (u, v))) = h(f (a, a), f (u, b)) y
θ2 (h(f (a, x), f (y, b))) = θ2 (h(z, f (u, v))) = h(f (a, x), f (u, b)).
además, θ2 es más general que θ1 en el sentido de que θ1 = {x/a} ◦ θ2
No existe un único unificador de máxima generalidad para dos términos dados t y s; sin embargo, dos
umgs para t y s son tales que uno de ellos se obtiene a partir del otro mediante la composición con una
sustitución de renombramiento:
Teorema 5.3 Si θ1 y θ2 son umgs para un conjunto de términos T entonces, existen dos sustituciones
de renombramiento λ1 y λ2 tales que λ1 ◦ θ1 = θ2 y λ2 ◦ θ2 = θ1 .
Este algoritmo siempre termina para cualquier conjunto finito no vacı́o de términos (de átomos), pues
en caso contrario se generarı́a una secuencia infinita σ0 T, σ1 T, . . . de conjuntos finitos y no vacı́os con la
propiedad de que cada uno de ellos tiene una variable menos que el anterior (es decir, σk T contiene xk
pero σk+1 T no), lo cual es imposible porque T (respectivamente A) sólo puede contener un número finito
de variables.
ee
rr
El algoritmo anterior es no determinista ya que en el paso (3) pueden existir varias elecciones
de xk y tk . Tiene un paso sumamente ineficiente, la verificación sistemática de la no ocurrencia
de una variable en un término (en la bibliografı́a inglesa: occurs check ).
En las implementaciones del algoritmo para sistemas de programación lógica, esta com-
probación simplemente se omite, aun a riesgo de perder la corrección del algoritmo y, en
consecuencia, con la posibilidad de obtener un resultado erróneo.
Demostración: Si T es unificable, y el algoritmo termina con la salida: “σk es el unificador más general
para T ”, es evidente que σk es un unificador; nos falta probar que σk es un umg, es decir, que para
cualquier otro unificador θ existe una sustitución λ tal que θ = λ ◦ σk .
Sea θ un unificador para T . Demostremos por inducción que para cada k natural θ = θ ◦ σk :
Ejemplo 5.11 Para los átomos P (a, x, f (g(y))) y P (z, f (z), f (u)) la ejecución es como sigue:
k = 0; σ0 = ǫ; D0 = Dis(P (a, x, f (g(y))), P (z, f (z), f (u))) = {a, z}
σ1 = {z/a}.
“σ3 es un umg”
Ejemplo 5.12 Para los átomos Q(f (a), g(x)) y Q(y, y) la ejecución es como sigue:
k = 0; σ0 = ǫ; D0 = Dis(Q(f (a), g(x)), Q(y, y)) = {f (a), y}
σ1 = {y/f (a)}.
Ejemplo 5.13 Para los átomos P (a, x, h(g(z))) y P (z, h(y), h(y)) la ejecución es como sigue:
k = 0; σ0 = ǫ; D0 = Dis(P (a, x, h(g(z))), P (z, h(y), h(y))) = {a, z}
σ1 = {z/a}.
D1 = {x, h(y)}
σ2 = {x/h(y)} ◦ {z/a} = {z/a, x/h(y)}.
D2 = {g(a), y}
σ3 = {y/g(a)} ◦ {z/a, x/h(y)} = {z/a, x/h(g(a)), y/g(a)}.
D3 = ∅
5.2. UNIFICACIÓN 125
“σ3 es un umg”
El concepto de unificación puede verse como el análogo a la resolución de ecuaciones en una teorı́a
algebraica, algo tan antiguo como la misma Matemática; en definitiva, la teorı́a de la unificación no
es más que la extensión de este estudio a un contexto más abstracto. Por esta razón, incluimos en esta
sección una segunda versión del algoritmo de unificación que, dado un conjunto de ecuaciones de términos,
determina si es o no unificable y, si lo es, proporciona un umg para tal conjunto.
El algoritmo termina cuando se llega a un error o no se puede aplicar ningún paso a ninguna ecuación.
126 CAPÍTULO 5. MÉTODO DE RESOLUCIÓN
ee
rr
El algoritmo anterior es, obviamente, no determinista y como la versión primera, tiene un
paso sumamente ineficiente, la verificación sistemática de la no ocurrencia de una variable
en un término.
Demostración:
Terminación Cualquier aplicación de los pasos 1. ó 3. disminuye estrictamente el número de ocurrencias
de variables y funciones que aparecen en las ecuaciones. El paso 4. sólo se puede aplicar un número
finito de veces antes de aplicar otro paso, y su aplicación no incrementa este número total. Después
de un número finito de aplicaciones de los pasos 1., 3. y 4. o el algoritmo termina o existe una
aplicación del paso 5.
La aplicación del paso 5. puede terminar o bien detectando un error y terminando la ejecución
o bien eliminando todas las ocurrencias de una variable en el miembro de la derecha de todas
las ecuaciones. En consecuencia, para cada variable el paso 5. sólo puede ser ejecutado una vez;
puesto que sólo hay un número finito de variables en el conjunto de ecuaciones, este paso sólo se
ejecutará un número finito de veces.
Según lo anterior, puesto que cada paso se ejecuta a lo sumo una cantidad finita de veces, el
algoritmo termina para todo conjunto de ecuaciones de entrada.
Corrección Supongamos que el algoritmo no ha terminado con error y que nos ha devuelto un conjunto
de ecuaciones E ′ , veamos que E es resoluble y que E ′ es un conjunto de ecuaciones en forma
resuelta equivalente a E.
Es fácil convencerse de que cada paso del algoritmo conserva las soluciones del conjunto de ecuacio-
nes. Esto se debe a que estamos tratando con la igualdad sintáctica (por ejemplo, f (u) = f (v) tiene
las mismas soluciones que u = v) y con la igualdad matemática (por eso si x = t podemos reem-
plazar x por t en el resto de las ecuaciones sin afectar el conjunto de soluciones). En consecuencia,
el conjunto de salida es equivalente al conjunto de entrada.
Los miembros de la derecha de las ecuaciones de E ′ son variables, ya que en otro caso se podrı́a
aplicar el paso 1., 2. ó 4. Todas estas variables son diferentes y no aparecen a la derecha de las
ecuaciones, ya que en tal caso se podrı́a aplicar el paso 5. Por lo tanto E ′ está en forma resuelta;
puesto que E es equivalente a E ′ entonces E es resoluble.
Supongamos ahora que el algoritmo termina con error, veamos que E no es resoluble.
Por el razonamiento anterior tenemos que el conjunto de ecuaciones que tenemos en la detección
del error es equivalente a E.
Si el error ocurrió en el paso 2, el conjunto E no es resoluble puesto que ninguna sustitución
de las variables va a conseguir unificar los sı́mbolos de función externos.
Si el error ocurrió en el paso 5, el conjunto E no es resoluble porque x = t no es resoluble.
Esto se debe a que la aplicación de cualquier sustitución básica a x produce en el miembro de
la derecha un término estrictamente mayor que en el de la izquierda, por lo que la identidad
sintáctica no es posible.
En todo lo que sigue sólo consideraremos conjuntos finitos de cláusulas de L1 , es decir, formas clausales.
Supondremos también que las cláusulas no contienen literales repetidos. Para este fin, cuando aparezca
una cláusula con literales repetidos, para cada uno de ellos se eliminan todas sus ocurrencias salvo la
ocurrencia situada más a la izquierda.
5.3. RESOLUCIÓN DE ÁTOMOS NO BÁSICOS 127
Del mismo modo que en el caso básico, las cláusulas C1 y C2 se denominan cláusulas paternas de C.
Es preciso destacar que en la definición de resolvente, es posible varios literales a la vez. Esta caracterı́stica
del método para la lógica de primer orden se conoce con el nombre de factorización. Consideremos, por
ejemplo, el conjunto de cláusulas Ω = {P (x) ∨ P (y), ¬P (x) ∨ ¬P (y)}. Este conjunto es insatisfacible. En
efecto,
Sin embargo, ninguna demostración por resolución que elimina únicamente un literal cada vez puede
producir 2. Este hecho motiva la definición siguiente.
Definición 5.10 Si dos o más literales (con el mismo signo) de una cláusula C son unificables con umg
σ entonces σC se dice que es un factor de C.
Definición 5.11 Una resolvente para las cláusulas C1 y C2 es una de las siguientes resolventes binarias:
1. Una resolvente binaria de C1 y C2 .
2. Una resolvente binaria de C1 y un factor de C2 .
3. Una resolvente binaria de un factor de C1 y C2 .
4. Una resolvente binaria de un factor de C1 y un factor de C2 .
es θ = {x/f (a), y/f (a), z/a, w/a}. Hallamos la resolvente mediante θ y obtenemos la cláusula
Definición 5.12 Dados un conjunto Ω de cláusulas y una cláusula C de L1 , se dice que C es deducible
por resolución a partir de Ω, denotado Ω ⊢R C, si existe una secuencia de cláusulas C1 , C2 , · · · , Cn tal
que
128 CAPÍTULO 5. MÉTODO DE RESOLUCIÓN
1. Cada Ci (1 ≤ i ≤ n) es o bien una cláusula de Ω o bien una resolvente de dos cláusulas anteriores
en la secuencia.
2. Cn = C.
La secuencia Ci (1 ≤ i ≤ n) se dice que es una deducción por resolución de C a partir de Ω.
Una deducción por resolución de 2 a partir de Ω se dice una refutación por resolución de Ω.
Veamos que la exigencia de que C1 y C2 no tengan variables en común es necesaria. Consideremos,
por ejemplo, el conjunto de cláusulas {P (f (x)), ¬P (x)}. Puesto que este conjunto representa a la fbf
(∀x)P (f (x)) ∧ (∀x)¬P (x), se trata de un conjunto de cláusulas insatisfacible; sin embargo, P (f (x)) y
P (x) no son unificables, porque no podemos hacer la sustitución x/f (x); esto se resuelve renombrando
las variables para obtener (∀x)P (f (x)) ∧ (∀y)¬P (y), es decir, el conjunto de cláusulas {P (f (x)), ¬P (y)},
cuyo umg es {y/f (x)}. Veamos otro ejemplo.
es la siguiente secuencia
1. P (x, a, y) de Ω.
2. ¬P (f (u), y, w) ∨ Q(v, g(a, x)) de Ω.
3. ¬Q(z, g(a, f (t))) de Ω.
4. Q(v, g(a, f (u))) de 1. y 2. (con umg σ = {x/f (u), y/a, w/a})
5. 2 de 3. y 4. (con umg σ = {z/v, t/u})
En el ejemplo anterior no ha sido preciso renombrar variables. Sin embargo, como nos muestra el siguiente
ejemplo, puede suceder que este renombramiento sea necesario.
Ejemplo 5.16 Consideremos el conjunto de cláusulas
En este caso, P (x, a, y) y ¬P (f (x), v, w) ∨ Q(v, g(a, x)) no son unificables ya que x ocurre en f (x).
Evitaremos esta situación renombrando x en la segunda cláusula, por ejemplo por u. De esta forma,
obtenemos el conjunto de cláusulas del ejemplo 5.15 para el que, como hemos visto, no existe ningún
problema.
Nuestro propósito es demostrar ahora que el principio de resolución con unificación es completo; esto es,
que un conjunto de cláusulas S es insatisfacible si y sólo si la cláusula vacı́a es deducible usando la regla
de resolución. Para ello necesitaremos el siguiente lema, que permitirá tomar como punto de partida una
refutación por resolución básica y contemplar su extensión a una resolución general.
Lema 5.1 (de extensión) Si C1′ y C2′ son instancias de C1 y C2 respectivamente, y si C ′ es una
resolvente de C1′ y C2′ entonces existe una resolvente C de C1 y C2 tal que C ′ es una instancia de C.
donde γ es un umg de L1 y L2 . Puesto que las cláusulas Ci′ son instancias de las cláusulas Ci , existe
una sustitución θ tal que Ci′ = θCi . Sean Li 1 , . . . , Li ri los literales de Ci que corresponden a Li , es decir,
5.3. RESOLUCIÓN DE ÁTOMOS NO BÁSICOS 129
aquellos que θLi 1 = · · · = θLi ri = L′i . Si ri > 1 obtengamos un umg λi para el conjunto {Li 1 , . . . , Li ri }
y sea Li = λi Li 1 . En tal caso Li es un literal del factor λi Ci de Ci . Si ri = 1 sea entonces λi = id y
Li = Li 1 . Sea λ = λ1 ∪ λ2 . Con esta definición de Li tenemos que L′i es una instancia de Li ; puesto que
L′1 y L′2 son unificables también tenemos que L1 y L2 son unificables. Sea σ un umg de L1 y L2 :
I(N ) = {m1 , m2 , . . . , mn }
I(N1 ) = {m1 , m2 , . . . , mn , mn+1 }
I(N2 ) = {m1 , m2 , . . . , mn , ¬mn+1 }
Puesto que N1 y N2 son nodos fallo pero N no lo es, deben existir dos instancias básicas C1′ y C2′ de
las cláusulas C1 y C2 tales que C1′ y C2′ son falsas en I(N1 ) e I(N2 ) respectivamente, pero no en I(N ).
Por lo tanto, C1′ debe contener a ¬mn+1 y C2′ debe contener a mn+1 . Sea L′1 = ¬mn+1 y L′2 = mn+1 ;
resolviendo respecto de los literales L′1 y L′2 obtenemos la resolvente
Ahora C ′ debe ser falsa en I(N ) puesto que tanto (C1′ − L′1 ) como (C2′ − L′2 ) son falsas en I(N ). Por el
lema de extensión, existe una resolvente C de C1 y C2 tal que C ′ es una instancia básica de C. Sea T ′′
el árbol semántico cerrado para (S ∪ {C}), obtenido de T ′ eliminando toda la parte que existe bajo el
primer nodo en el que la resolvente C ′ es falsificada. Claramente, el número de nodos de T ′′ es menor
que el de T ′ . Aplicando este mismo proceso a T ′′ podemos obtener otra resolvente de las cláusulas de
(S ∪ {C}) que, añadida a (S ∪ {C}) nos permite encontrar un árbol todavı́a más pequeño. Este proceso se
aplica tantas veces como sea necesario hasta obtener un árbol que sólo tenga el nodo raı́z. Esto es posible
sólo cuando 2 es deducible, por lo tanto existe una deducción de 2 a partir de S.
Para la demostración del recı́proco supongamos que existe una deducción de 2 a partir de S. Sean
R1 , R2 , . . . , Rk las resolventes de tal deducción. Supongamos que S es satisfacible, entonces existe un
130 CAPÍTULO 5. MÉTODO DE RESOLUCIÓN
modelo M de S. Sin embargo, si un modelo satisface las cláusulas resolubles C1 y C2 también satisface
a su resolvente; por lo tanto M satisface a R1 , R2 , . . . , Rk , lo cual es imposible puesto que una de estas
cláusulas es 2. Por lo tanto S es insatisfacible.
Ω = {P (x) ∨ Q(x) ∨ R(x, f (x)), ¬P (z) ∨ Q(z) ∨ S(f (z)), T (a), P (a),
¬R(a, y) ∨ T (y), ¬T (u) ∨ ¬Q(u), ¬T (w) ∨ ¬S(w)}
8. 2 de 5. y 7.
En los ejemplos anteriores la búsqueda de una refutación se ha realizado de modo arbitrario, sin embargo,
es obvio es necesario una sistematización para esta búsqueda. El modo más simple (conceptualmente
hablando) de sistematizar la búsqueda de una refutación o bien la de asegurar que no existe, se basa en la
generación sucesiva de todas las posibles resolventes a partir del conjunto Ω de partida. más precisamente:
Dado un conjunto de cláusulas Ω, denotamos por R(Ω) la unión de Ω y el conjunto de todas las resolventes
de cláusulas de Ω (resolventes obtenidas utilizando sólo cláusulas de Ω). Para todo n ∈ N, definimos Rn (Ω)
como sigue:
R0 (Ω) = Ω
Rn+1 (Ω) = R(Rn (Ω))
1. P ∨ Q
2. P ∨ R
3. ¬Q ∨ ¬R
4. ¬P
5. P ∨ ¬R (por 1 y 3)
6. Q (por 1 y 4)
7. P ∨ ¬Q (por 2 y 3)
8. R (por 2 y 4)
R(Ω) = Ω ∪ {P ∨ ¬R, Q, P ∨ ¬Q, R}
9. P (por 1 y 7)
10.
— P (por 2 y 5)
10. ¬R (por 3 y 6)
11. ¬Q (por 3 y 8)
— ¬R
12. (por 4 y 5)
— ¬Q
12. (por 4 y 7)
12.
— P (por 5 y 8)
132 CAPÍTULO 5. MÉTODO DE RESOLUCIÓN
12.
— P (por 6 y 7)
2
R (Ω) = R(Ω) ∪ {P, ¬R, ¬Q}
12.
— P (por 1 y 11)
12.
— P (por 2 y 10)
12. 2 (por 4 y 9)
Las lı́neas tachadas indican que las resolventes generadas se eliminan por estar ya en la secuencia.
Una primera estrategia consiste en la no inclusión de las resolventes que ya están en Si . Esto conlleva
un menor gasto en la generación de cada nivel pero, en cualquier caso, el tiempo gastado al calcular las
resolventes que después se van a eliminar no es recuperable.
Como en el caso proposicional, existen otros refinamientos mucho más depurados del método de resolución
que se presentan en la siguiente sección; todos ellos incluyen como simplificación la eliminación de aquellas
cláusulas generadas por resolución que o bien contienen un literal y su opuesto o contienen otra cláusula
ya generada.
C0 , B0 , C1 , B1 , . . . , Cn−1 , Bn−1 , Cn
tal que
1. C0 ∈ Ω.
4. Cn = C.
El modo habitual de representar este tipo de deducciones es mediante un árbol binario, llamado árbol de
resolución lineal, de la forma
5.3. RESOLUCIÓN DE ÁTOMOS NO BÁSICOS 133
C0 B0
C1 B1
C2 Bn−2
..
.
Bn−1
Cn−1
P ∨Q ¬P ∨ Q
Q ¬Q ∨ R
R ¬Q ∨ ¬R
¬Q Q
Las cláusulas laterales son ¬P ∨ Q, ¬Q ∨ R, ¬Q ∨ ¬R de Ω y Q. Ésta es, además, una cláusula central.
Ejemplo 5.21 Presentamos tres ejemplos de resolución lineal ordenada de dos cláusulas dadas:
1. La resolvente de P ∨ ¬Q ∨ R y P ∨ ¬R ∨ T es P ∨ ¬Q ∨ R ∨ T .
2. La resolvente de P ∨ ¬Q ∨ R y P ∨ ¬R es P ∨ ¬Q, obtenida mediante las siguientes simplificaciones:
Con relación a la resolución lineal, la resolución lineal ordenada no sólo reduce el número de resolventes por
considerar debido al hecho de resolver únicamente respecto del último literal, sino que además incorpora
una nueva estrategia de eficiencia considerando un determinado tipo de cláusulas respecto de las cuales
sólo se requiere resolver con cláusulas centrales.
Definición 5.14 Una cláusula ordenada se denomina cláusula ordenada reducible si su último literal
es el opuesto de algún literal enmarcado de dicha cláusula. Si C es una cláusula ordenada reducible, la
cláusula ordenada obtenida al eliminar el último literal de C se denomina cláusula reducida de C.
Si la cláusula Ci por resolver es reducible, se puede demostrar que sólo será necesario resolver con cláusulas
centrales y existe una cláusula central Cj tal que R(Ci , Cj ) es la reducida de Ci .
Disponemos ya de los elementos necesarios para definir la deducción en la resolución lineal ordenada.
Definición 5.15 Sea Ω un conjunto de cláusulas ordenadas y C0 ∈ Ω. Una deducción lineal ordenada
de una cláusula C a partir de Ω con cabeza C0 es una secuencia de cláusulas ordenadas
C0 , B0 , C1 , B1 , . . . , Cn−1 , Bn−1 , Cn
tal que
1. Para todo i = 0, 1, 2, . . . , n − 1, Bi ∈ Ω o Bi = Cj para algún j con j < i.
2. Para todo i = 2, . . . , n, si Ci−1 es reducible, entonces Ci es la reducida de Ci−1 y en caso contrario,
Ci es la resolvente ordenada de Ci−1 y Bi con Bi ∈ Ω.
5.3. RESOLUCIÓN DE ÁTOMOS NO BÁSICOS 135
3. Cn = C.
C0 , B0 , C1 , B1 , . . . , Cn−1 , Bn−1 , Cn
se representa
C0 B0
C1 B1
C2 . Bn−2
..
Cn−1 Bn−1
En el caso en que C = 2, este árbol se dice que es un árbol de refutación lineal ordenada para Ω.
Ejemplo 5.22 Un árbol de refutación lineal ordenada para
Ω = {P ∨ Q, ¬P ∨ Q, ¬Q ∨ ¬R, ¬Q ∨ R}
P ∨ Q ∨ ¬R ¬Q ∨ R
P ∨ Q ∨ ¬R ∨ ¬Q (. . . P ∨ Q)
P ¬P ∨ Q
P ∨Q ¬Q ∨ R
P ∨ Q ∨R ¬Q ∨ ¬R
P ∨ Q ∨ R ∨ ¬Q (. . . P ∨ Q)
Los puntos suspensivos en el árbol de refutación indican que la correspondiente cláusula lateral no se
requiere, puesto que se ha aplicado una reducción (en la cláusula central aparece un literal encuadrado y
su opuesto sin encuadrar).
C0 •
B0
C1 •
B1
C2 •
..
.
Cn−1 •
Bn−1
Cn •
y para cada proceso de cabeza C0 , se utiliza un árbol con raı́z etiquetada con la cláusula cabeza C0 . El
árbol se genera (primero en anchura o primero en profundidad) de forma que cada nivel de profundidad
representa una etapa. Las ramas del árbol ası́ generado son, por lo tanto, deducciones lineales ordenadas
de cabeza C0 .
Ejemplo 5.23 Dado el conjunto Ω formado por las siguientes cláusulas
justifican el renombramiento.
5.4. CLÁUSULAS DE HORN 137
Tras renombrar tenemos un conjunto Ω′ simultáneamente satisfacible con Ω con las siguientes cláusulas
¬R(x, y) ∨ ¬D(y) ∨ ¬H(f (x), y) ∨ S(x)
¬P (z) ∨ D(z)
R(u, g(v))
H(f (w), g(r))
¬S(g(a))
P (s) ∨ S(s)
P (t) ∨ D(q) ∨ H(b, t)
donde q, r, s, t, u, v, w, x, y, z son sı́mbolos de variables y a y b sı́mbolos de constantes.
En la Figura 5.1 aparece un árbol de refutación lineal ordenada para el conjunto Ω′ , donde en cada arco
del árbol aparece la cláusula lateral respecto de la que se resuelve y las sustituciones proporcionadas por
el unificador de mayor generalidad.
C ≡ (P1 ∧ . . . ∧ Pn ) → Q
y por tanto,
¬S(g(a))
x/g(a)
P (s) ∨ S(s)
P (t) ∨ D(q) ∨ H(b, t)
s/g(r)
t /g(r)
¬S(g(a))
r/a
¬R(g(a), g(a))
R(u, g(r))
u/g(a), r/a
Figura 5.1:
5.4. CLÁUSULAS DE HORN 139
1. Puesto que se trata de una programación basada en conocimiento, permite caracterizaciones sim-
ples y precisas de relaciones entre los programas y los resultados computados por ellos; entre los
programas y sus especificaciones y entre diversos programas.
3. Proporciona un paradigma uniforme para la tecnologı́a del software: un solo paradigma sirve para
construir y manipular programas, especificaciones, bases de datos y herramientas software asocia-
das.
4. Puede ser modificada o extendida de modo natural para recoger formas especiales de conocimiento
tales como conocimiento de orden superior o metanivel.
La tarea de escribir un programa toma como punto de partida una especificación que describe con mayor
o menor detalle cómo ha de comportarse un programa. Esta especificación puede ser una declaración
informal en lenguaje natural de los requisitos que ha de satisfacer el programa; o puede ser formal, es
decir, un documento técnico que recoge de forma precisa el comportamiento exacto que ha de tener el
programa.
La ventaja de las especificaciones formales son evidentes a posteriori, es decir, cuando después de escribir
el programa, deseamos examinar si su comportamiento se ajusta a la especificación.
Si la especificación utiliza la lógica, podemos expresar las relaciones entre bloques simples del programa
y los comportamientos de éstos para, posteriormente, a partir del modo de combinación de estos bloques,
utilizar las técnicas de la lógica para determinar el comportamiento del programa total.
Los primeros trabajos sobre verificación de programas utilizando la lógica se deben a Floyd y Hoare. Pero
el avance más significativo se debe al trabajo de Z. Manna y A. Pnueli, que utiliza la lógica temporal para
especificación y verificación de programas paralelos. En este trabajo, se utiliza la lógica tanto para expresar
hechos del programa como para describir su comportamiento. De este modo, la lógica puede usarse para
establecer si las declaraciones sobre el comportamiento del programa se derivan de las declaraciones que
constituyen el programa.
Si consideramos el desarrollo del método en forma de árbol de resolución, el abandono de una rama para
continuar la búsqueda por la siguiente rama se denomina backtracking.
5.4. CLÁUSULAS DE HORN 141
5.4.1.1. Prolog
Prolog es un lenguaje de programación lógica; se utiliza cuando queremos que el ordenador resuelva
problemas que puedan expresarse en términos de objetos y relaciones entre ellos.
Este formalismo de programación añade al sistema lógico central (es decir, a la conjunción: “lógica en
forma clausal y resolución”) un tipo particular de estrategia de control con el propósito de obtener
una implementación eficiente. Como paradigma declarativo, se caracteriza porque el análisis lógico de los
programas no considera aspectos de comportamientos. En este caso, se habla de Prolog puro.
No obstante, el término Prolog tiene además otras connotaciones referidas a estrategias de control,
por ejemplo, añade primitivas no lógicas dando lugar a un nuevo formalismo conocido como Prolog
impuro. Muchas de estas primitivas contemplan aspectos de comportamientos a expensas de “corromper”
el formalismo lógico básico.
En sı́ntesis, la programación en Prolog consiste en:
1. Declarar algunos hechos sobre los objetos y sus relaciones
2. Definir algunas reglas sobre los objetos y sus relaciones.
3. Hacer “preguntas” sobre los objetos y sus relaciones.
Cuando se hace una pregunta a Prolog, éste efectuará una búsqueda por toda la base de conocimiento
(colección de hechos y reglas) introducida previamente. Buscará hechos que coincidan con el hecho en
cuestión. Si no lo encuentra, intentará encontrar la respuesta mediante las reglas. En definitiva,
Prolog = Proceso de obtención de respuesta en cláusulas de Horn.
+ Sistema de gestión de archivos de cláusulas.
+ Cláusulas predefinidas (aritméticas, etc).
+ Funciones para controlar el proceso de búsqueda.
+ Funciones para controlar el proceso de unificación
En Prolog las cláusulas se escriben en forma procedural :8
T : − P, Q, R, S
5. : − S(a)
6. : − Q(y), R(a, y) de 1. y 5. para el umg x/a.
7. : − P (y), R(a, y) de 2. y 6. para el umg x/y.
8. : − R(a, b) de 3. y 7. para el umg y/b.
9. 2 de 4. y 8.
Como ¬R(x, b) no encuentra ninguna cláusula resoluble con ella, la rama se poda y se realiza un back-
tracking para ejecutar con la cláusula S(x) ∨ ¬T (x) .
Teorema 5.7 Dado un programa lógico P la intersección de todos los modelos de Herbrand para P es
el mı́nimo modelo de Herbrand para P.
Demostración: Probemos en primer lugar que todo programa lógico es satisfacible, es decir, tiene un
modelo de Herbrand. En efecto, consideremos MH,Ω = (HΩ , IH,Ω ) donde
Teorema 5.8 Dado un programa lógico P el mı́nimo modelo de Herbrand para P es el conjunto de todos
los átomos básicos que son consecuencia lógica de P.
b
Demostración: Sea ConTAtom (P) el conjunto de todos los átomos básicos que son consecuencia semánti-
ca de P y sea mmH (P) = i∈I MiH,P la intersección de todos los modelos de Herbrand para P. Tenemos
que probar que
ConbAtom (P) = mmH (P)
Por definición de consecuencia semántica, es obvio que
Inversamente, sea P ∈ mmH (P). Tenemos que probar que cualquier modelo M de P es un modelo de P .
Por definición de P , esto es cierto si M = (D, I) es un modelo de Herbrand. Supongamos que M = (D, I)
no es un modelo de Herbrand. Como vimos en la demostración del Teorema 2.1, {Q ∈ BH,P | I(Q) = 1}
es un modelo de Herbrand para P y puesto que P es verdadera para todo modelo de Herbrand de P, se
tiene que I(P ) = 1. Por lo tanto,
mmH (P) ⊆ ConbAtom (P)
9
Puesto que los modelos de Herbrand son subconjuntos de la base de Herbrand, la relación de inclusión
conjuntista, ⊆, establece un orden en el conjunto de los modelos de Herbrand. Existe entonces un modelo de
Herbrand minimal al que se denomina modelo mı́nimo de Herbrand de P
144 CAPÍTULO 5. MÉTODO DE RESOLUCIÓN
5.5. Ejercicios
1. Definir por inducción estructural la noción de sustitución finita sobre el conjunto Term de términos
de L1 .
2. Dado el átomo P (x, y, z, t) y las sustituciones
θ1 = {x/f (y), y/g(w), z/v}; θ2 = {x/a, y/b, w/f (y), v/z, t/c}
(θ2 ◦ θ1 )P (x, y, z, t)
3. Hallar, si existe, un unificador para cada uno de los siguientes conjuntos de átomos
a) {P (x, f (y), z), P (g(a), f (w), u), P (v, f (b), c)}
b) {Q(h(x, y), w), Q(h(g(v), a), f (v)), Q(h(g(v), a), f (b))}
4. Hallar el conjunto de discrepancias para los conjuntos de términos:
a) {f (x, x), f (y, g(y))}
b) {f (x, g(y)), f (h(y), g(h(z)))}
c) {f (h(x), g(x)), f (g(x), h(x))}
5. Hallar, si existe, un umg para cada uno de los siguientes pares de átomos
a) P (x, a) y P (b, c)
b) P (f (x), y)) y P (f (a), z)
c) P (f (x), y)) y P (b, z)
d ) P (x, a) y P (b, a)
e) P (x, f (a, x)), P (b, y)
f ) Q(x, f (g(a, x), z)) y Q(b, f (g(a, f (w, c)), h(y, x)))
g) P (f (y, g(z)), h(b)) y P (f (h(b), g(z)), y)
h) P (a, f (b, f (c, x))) y P (a, y)
i) R(x, f (g(a, y), z)) y R(b, f (g(a, f (w, c)), h(y, x)))
j ) Q(x, f (a, f (y, c))) y Q(z, f (z, f (f (a, c), w)))
k ) Q(f (a), g(x)) y Q(y, y)
l ) P (a, x, h(g(z))) y P (z, h(y), h(y))
6. Determine si las siguientes cláusulas tienen factores y en tal caso determı́nelos:
7. Hallar todas las resolventes para cada uno de los siguientes pares de cláusulas
a) ¬P (x) ∨ Q(x, b) y P (a) ∨ Q(a, b)
b) ¬P (x) ∨ Q(x, x) y ¬Q(a, f (a))
c) ¬P (x, y, u) ∨ ¬P (y, z, v) ∨ ¬P (x, v, w) ∨ P (u, z, w), y P (g(x, y), x, y)
d ) ¬P (v, z, v) ∨ P (w, z, w) y P (w, h(x, x), w)
146 CAPÍTULO 5. MÉTODO DE RESOLUCIÓN
11. Aplicar resolución lineal ordenada para analizar la satisfacibilidad o no del conjunto de cláusulas
{P (x) ∨ Q(x) ∨ R(x, f (x)), ¬P (z) ∨ Q(z) ∨ S(f (z)), T (a), P (a),
R(a, y) ∨ T (y), ¬T (u) ∨ ¬Q(u), ¬T (w) ∨ ¬S(w)}
P (y, a) ∨ P (f (y), y)
P (y, a) ∨ P (y, f (y))
¬P (x, y) ∨ P (f (y), y)
¬P (x, y) ∨ P (y, f (y))
¬P (x, y) ∨ ¬P (y, a)
5.5. EJERCICIOS 147
16. Para cada una de las fórmulas siguientes, A: determine una fórmula en forma normal de Skolem
equisatisfacible con A y determine su universo y base de Herbrand; determine una fórmula en forma
normal de Skolem equisatisfacible con ¬A y determine su universo y base de Herbrand.
a) (∀x)P (x) → (∃x)Q(x)
b) (∀x)(P (x) → (∃y)R(y))
c) (∀x)(P (x) → (∃y)Q(x, y))
d ) (∃x)(¬(∃y)P (y) → (∃z)(Q(z) → R(x)))
e) (∀x)(∀y) (∃z)P (z) ∧ (∃u)(Q(x, u) → (∃v)Q(y, v)))
f ) (∀x)(∀y) (∃z)(P (x, z) ∧ P (y, z)) → (∃u)Q(x, y, u)
g) (∀x)(∀y)(∀z)((P (x, y) ∧ P (y, z)) → Q(x, z)) ∧ ((∀x)(∃y)P (x, y) → (∀x)(∃y)Q(x, y))
17. Dado el razonamiento:
(∀x) (∃y) E(x) ∧ C(x, y) → S(x) ∧ (∀z)(C(z, x) → S(z))
(∀x)(∀y) (P (x) ∧ C(y, x)) → R(y)
———————————————————————————
(∀x) P (x) ∧ (∃y)(E(y) ∧ C(x, y)) → (∀z) C(z, x) → (R(z) ∧ S(z))
21. Aplicar resolución lineal ordenada para analizar la validez o no del razonamiento siguiente:
Ningún vendedor de coches usados compra un coche usado para uso familiar.
Algunos de los que compran un coche usado para uso familiar son deshonestos.
22. Aplicar resolución lineal ordenada para analizar la validez o no de los siguientes razonamientos:
a) Todo estudiante es honesto, Juan no es honesto; por lo tanto Juan no es estudiante.
148 CAPÍTULO 5. MÉTODO DE RESOLUCIÓN
b) Todo atleta es fuerte, todo el que es fuerte e inteligente triunfará en su carrera, Pedro es un
atleta, Pedro es inteligente; por lo tanto Pedro triunfará en su carrera.
c) Todo aquel que ama a alguien ama a San Francisco, no hay nadie que no ame a nadie; por lo
tanto todo el mundo ama a San Francisco.
23. Dado el programa Prolog:
Comprende(lógica-comput-I,x) :− Atiende(x, clases)
Atiende(x, clases) :− Responsable(x)
Responsable(carlos)
a) Inferir de este programa que Carlos comprende la asignatura.
b) ¿Se puede inferir de este programa que Carlos no es responsable?
c) ¿Qué objetivos atómicos se puede inferir de este programa?