PDF de programación - Tema 8: Teorema de Herbrand. Tableros en lógica de primer orden

Tema 8:

Teorema de Herbrand. Tableros en lógica de

primer orden

Dpto. Ciencias de la Computación Inteligencia Artificial

Universidad de Sevilla

Lógica Informática

(Tecnologías Informáticas)

Curso 2014–15

Teorema de
Herbrand.
Tableros

Reducción a la
lógica
proposicional
Teorema de Herbrand

Fórmulas δ y γ

Tableros completos

Búsqueda de
modelos

Consecuencia
lógica

Razonamiento con
igualdad

Contenido

Reducción a la lógica proposicional

Teorema de Herbrand

Fórmulas δ y γ

Tableros completos

Búsqueda de modelos

Consecuencia lógica

Razonamiento con igualdad

Teorema de
Herbrand.
Tableros

Reducción a la
lógica
proposicional
Teorema de Herbrand

Fórmulas δ y γ

Tableros completos

Búsqueda de
modelos

Consecuencia
lógica

Razonamiento con
igualdad

Reducción a la lógica proposicional

Sea Γ un conjunto de fórmulas de un lenguaje L.

El cálculo de formas de Skolem reduce la consistencia

de Γ a la consistencia de un conjunto Σ de
fórmulas abiertas (de hecho, cláusulas) en un nuevo
lenguaje L (que extiende a L con nuevos símbolos).

Es posible dar un paso más y reducir la consistencia de

Γ a la consistencia de un conjunto de fórmulas
abiertas y cerradas.

Una fórmula abierta y cerrada puede identificarse con su

esqueleto proposicional y, por tanto, considerarse una
fórmula proposicional.

Definición. Sea Σ un conjunto de fórmulas abiertas. La
extensión de Herbrand de Σ, es el conjunto, EH(Σ),
formado por todas las fórmulas cerradas que pueden
obtenerse sustituyendo, de todas las formas posibles, las
variables de las fórmulas de Σ por términos cerrados.

Teorema de
Herbrand.
Tableros

Reducción a la
lógica
proposicional
Teorema de Herbrand

Fórmulas δ y γ

Tableros completos

Búsqueda de
modelos

Consecuencia
lógica

Razonamiento con
igualdad

Teorema de
Herbrand.
Tableros

Reducción a la
lógica
proposicional
Teorema de Herbrand

Fórmulas δ y γ

Tableros completos

Búsqueda de
modelos

Consecuencia
lógica

Razonamiento con
igualdad

Teorema de Herbrand

Teorema. Sea Σ un conjunto de fórmulas abiertas.
Son equivalentes:

1. Σ tiene un modelo.

2. EH(Σ) tiene un modelo.

3. EH(Σ) es satisfactible proposicionalmente.

Es decir, si identificamos cada fórmula de EH(Σ) con su

esqueleto proposicional, entonces el conjunto de
fórmulas proposicionales así obtenido es satisfactible.

Observaciones.

Este resultado reduce la consistencia de Σ a la de un

conjunto de fórmulas proposicionales: EH(Σ).

EH(Σ) puede ser un conjunto infinito. Sin embargo,
(Compacidad) Si EH(Σ) es inconsistente, entonces

existe un subconjunto finito Σ0 de EH(Σ) que es
inconsistente.

Ejemplo

El conjunto

Σ = {p(x) → p(f (f (x))),¬p(f (f (f (x)))), p(f (a))} es
inconsistente.

Su extensión de Herbrand EH(Σ), contiene entre otras

las fórmulas
1. p(f (a))
2. p(a) → p(f (f (a)))}
3. ¬p(f (f (f (a))))
4. p(f (a)) → p(f (f (f (a))))
5. ¬p(f (f (f (f (a)))))
6. p(f (f (a))) → p(f (f (f (f (a)))))}
7. ¬p(f (f (f (f (f (a))))))

...

[{x/a}]
[{x/a}]
[{x/f (a)}]
[{x/f (a)}]
[{x/f (f (a))}]
[{x/f (f (a))}]

El subconjunto de EH(Σ) formado por las fórmulas 1, 3

y 4 es inconsistente.

Teorema de
Herbrand.
Tableros

Reducción a la
lógica
proposicional
Teorema de Herbrand

Fórmulas δ y γ

Tableros completos

Búsqueda de
modelos

Consecuencia
lógica

Razonamiento con
igualdad

Teorema de
Herbrand.
Tableros

Reducción a la
lógica
proposicional
Teorema de Herbrand

Fórmulas δ y γ

Tableros completos

Búsqueda de
modelos

Consecuencia
lógica

Razonamiento con
igualdad

Tableros Semánticos

Recordemos que el método de los tableros semánticos

organiza de manera sistemática la búsqueda de
modelos, reduciendo la satisfactibilidad de las fórmulas
consideradas a la de ciertos conjuntos de literales.
En el caso de la lógica proposicional el método de

tableros semánticos clasifica las fórmulas en dos clases:
Las fórmulas α, que se comportan como conjunciones
Las fórmulas β, que se comportan como disyunciones

y asocia a cada fórmula, F , otras dos fórmulas más

sencillas (sus componentes) de modo que la
satisfactibilidad de F se reduce a la de sus componentes.
tener en cuenta los cuantificadores: ∃ y ∀.

Para extenderlo a la lógica de primer orden deberemos

Se introducen dos nuevas clases de fórmulas:

Las fórmulas de tipo γ que se comportan como

fórmulas cuantificadas universalmente, y

Las fórmulas de tipo δ, que se comportan como

fórmulas cuantificadas existencialmente.

Fórmulas de tipo γ

Las fórmulas de tipo γ son las siguientes:

γ
∀x F
F [x/t]
¬∃x F ¬F [x/t]

γt

(t es un término cerrado)
(t es un término cerrado)

Los términos cerrados son términos sin variables y se

denominan también términos básicos.

Las fórmulas γt son las componentes de γ.
Para satisfacer una fórmula de tipo γ es necesario

satisfacer simultáneamente todas sus componentes γt,
para todo término cerrado t.

Teorema de
Herbrand.
Tableros

Reducción a la
lógica
proposicional
Teorema de Herbrand

Fórmulas δ y γ

Tableros completos

Búsqueda de
modelos

Consecuencia
lógica

Razonamiento con
igualdad

Fórmulas de tipo δ

Las fórmulas de tipo δ son las siguientes:

δ
∃x F
F [x/a]
¬∀x F ¬F [x/a]

δa

(a es una nueva constante)
(a es una nueva constante)

Las fórmulas δa son las componentes de δ.
Para satisfacer una fórmula de tipo δ es necesario y

suficiente satisfacer alguna de sus componentes δa, para
alguna nueva constante a.

Teorema de
Herbrand.
Tableros

Reducción a la
lógica
proposicional
Teorema de Herbrand

Fórmulas δ y γ

Tableros completos

Búsqueda de
modelos

Consecuencia
lógica

Razonamiento con
igualdad

Reglas γ y δ

Reducen la consistencia de un conjunto de fórmulas U a la
de otro conjunto U formado por fórmulas más sencillas.

Regla γ: Si F ∈ U es de tipo γ, entonces

U consistente ⇔ U∪{γt : t término básico } consistente

Regla δ: Si F ∈ U es de tipo δ, entonces para cada

constante nueva, a, se tiene:
U consistente ⇐⇒ (U − {F}) ∪ {δa} consistente

Teorema de
Herbrand.
Tableros

Reducción a la
lógica
proposicional
Teorema de Herbrand

Fórmulas δ y γ

Tableros completos

Búsqueda de
modelos

Consecuencia
lógica

Razonamiento con
igualdad

Ejemplo
El conjunto U = {∃x Q(x), ∀x (Q(x) → R(x)), ∀x ¬R(x)}
es insatisfactible:

∃x Q(x), ∀x (Q(x) → R(x)), ∀x ¬R(x)

Q(a), ∀x (Q(x) → R(x)), ∀x ¬R(x)

Q(a), Q(a) → R(a), ∀x ¬R(x)



HHHHHH

Q(a), R(a), ¬R(a)

×

Q(a), ¬Q(a), ∀x ¬R(x)

Q(a), R(a), ∀x ¬R(x)

×

Teorema de
Herbrand.
Tableros

Reducción a la
lógica
proposicional
Teorema de Herbrand

Fórmulas δ y γ

Tableros completos

Búsqueda de
modelos

Consecuencia
lógica

Razonamiento con
igualdad

Notación

En lógica de primer orden representaremos los tableros etiquetando
cada nodo con una fórmula. El tablero anterior se escribirá:

∃x Q(x)

∀x (Q(x) → R(x))

∀x ¬R(x)

Q(a)

Q(a) → R(a)
 HH
¬Q(a)×

R(a)

¬R(a)×

Notación: Si l es un nodo de T , ahora U(l) es el conjunto de las
fórmulas que etiquetan los antecesores de l en T y el propio nodo
l.

Teorema de
Herbrand.
Tableros

Reducción a la
lógica
proposicional
Teorema de Herbrand

Fórmulas δ y γ

Tableros completos

Búsqueda de
modelos

Consecuencia
lógica

Razonamiento con
igualdad

Teorema de
Herbrand.
Tableros

Reducción a la
lógica
proposicional
Teorema de Herbrand

Fórmulas δ y γ

Tableros completos

Búsqueda de
modelos

Consecuencia
lógica

Razonamiento con
igualdad

Construcción de un tablero completo
Un tablero para F (un árbol T , con nodos etiquetados por
fórmulas y cuya raíz está etiquetado por F ) se construye
mediante el siguiente procedimiento:

Para cada hoja l de T , ni abierta ni cerrada, hacer:

1. Si existe un par de literales complementarios en U(l),

marcar con × (y se denomina hoja cerrada).

2. Si no existe tal par pero existe alguna fórmula en U(l)
no usada (en la rama de l), elegir A en U(l) no usada:
2.1 Si A es de tipo α, entonces, añadir un hijo l de l

etiquetado con α1 y otro hijo l de l etiquetado con
α2 y marcar A como usada en l.
2.2 Si A es de tipo β, añadir dos hijos a l: l con etiqueta
β1 y l con β2. Marcar A como usada (en l y l).
2.3 Si A es de tipo δ, añadir un hijo l de l con etiqueta δa
(a una nueva constante). Marcar A como usada en l.
lenguaje del tablero) tal que γt /∈ U(l), elegir uno de
tales términos y añadir un hijo con etiqueta γt .

2.4 Si A es de tipo γ y existe un término básico (del

3. Si no es posible extender l mediante las reglas

anteriores marcarla con (hoja abierta).

Teorema de
Herbrand.
Tableros

Reducción a la
lógica
proposicional
Teorema de Herbrand

Fórmulas δ y γ

Tableros completos

Búsqueda de
modelos

Consecuencia
lógica

Razonamiento con
igualdad

Propiedades de los tableros completos

Un tablero completo es un tablero construido
siguiendo las reglas anteriores y que no puede
extenderse más.

Un tablero T es cerrado si todas sus hojas son
Un tablero para un conjunto de fórmulas {A1, . . . , An}

cerradas. En otro caso es abierto.
es un tablero para la fórmula A1 ∧ ··· ∧ An.

Decimos que un conjunto de fórmulas S admite un

tablero completo cerrado si existe un tablero completo
para S que es cerrado.

Teorema. (Corrección y Completitud)
Sea S un conjunto de fórmulas cerradas.

1. Corrección: Si S admite un tablero completo y

cerrado, entonces S es inconsistente.

2. Completitud: Si S es inconsistente, entonces S admite

un tablero completo y cerrado.

Teorema de
Herbrand.
Tableros

Reducción a la
lógica
proposicional
Teorema de Herbrand

Fórmulas δ y γ

Tablero