PDF de programación - Tema 4: Resolución Proposicional

Resolución

proposicional

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

Tema 4:

Resolución Proposicional

Dpto. Ciencias de la Computación Inteligencia Artificial

Universidad de Sevilla

Lógica Informática

(Tecnologías Informáticas)

Curso 2015–16

Contenido

Sistemas deductivos
Pruebas formales
Encadenamiento con cláusulas de Horn

Resolución

La regla de resolución
Saturación
Estrategias de resolución

Resolución

proposicional

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

Pruebas formales

Resolución

proposicional

Los tableros semánticos proporcionan un algoritmo para

la deducción basado en este hecho:
{A1, . . . , An} |= A ⇐⇒ {A1, . . . , An,¬A} insatisfactible

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

Un enfoque más natural del problema básico (PB) que

presentamos en el Tema 1, se obtiene a través de la
noción de demostración:
1. Consideramos el conjunto de enunciados, BC, como un
conjunto de axiomas (o hipótesis que asumimos como
ciertas inicialmente).
2. El enunciado φ será consecuencia de BC si podemos
obtener una demostración de φ a partir de BC (de
manera similar a como en matemáticas se demuestra un
teorema).

Sistemas deductivos

Un sistema deductivo, T, (o teoría proposicional) consta
de:

Un conjunto, Ax(T), de fórmulas proposicionales que

llamamos los axiomas de T.

Reglas de inferencia de la forma:

Resolución

proposicional

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

A1, . . . , An

A

siendo A1, . . . , An, A fórmulas proposicionales. Las
fórmulas A1, . . . , An se denominan premisas y la
fórmula A conclusión.

Pruebas y teoremas

Una demostración en T es una sucesión de fórmulas

proposicionales A1, . . . , Ak cada una de las cuales es un
axioma de T, o bien, se obtiene a partir de fórmulas
anteriores de la sucesión mediante una regla de
inferencia.

Una fórmula A es un teorema de T, T A, si existe una

demostración en T, A1, . . . , Ak tal que A = Ak . La
sucesión A1, . . . , Ak se denomina una demostración de
A en T.

Resolución

proposicional

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

Ejemplo: Sistema deductivo

Axiomas de T: {p, q, p ∧ q → (¬s ∨ p → r )}
Reglas de inferencia:

(A y B fórmulas cualesquiera)

I∧ :

C∨ :

A, B
A ∧ B
A ∨ B
B ∨ A

I∨ :

MP :

A
A ∨ B
A, A → B

B

Resolución

proposicional

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

Ejemplo: demostración

La siguiente sucesión es una demostración de r en T; luego
T r

1. p
2. q
3. p ∧ q
4. p ∧ q → (¬s ∨ p → r )
5. ¬s ∨ p → r
6. p ∨ ¬s
7. ¬s ∨ p
8.

r

[[Hip.]]
[[Hip.]]
[[I∧ aplicada a 1. y 2.]]
[[Hip.]]
[[MP aplicada a 3. y 4.]]
[[I∨ aplicada a 1.]]
[[C∨ aplicada a 6.]]
[[MP aplicada a 7. y 5.]]

Resolución

proposicional

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

Procedimientos de demostración

Un sistema deductivo introduce una noción de prueba

formal, pero no proporciona ningún procedimiento
efectivo para generar demostraciones de las fórmulas
que deseamos probar.

Un sistema de razonamiento proporciona, además de

un sistema deductivo, un procedimiento de
demostración, que implementa una estrategia de
búsqueda de demostraciones.

Podemos ilustrar esta idea en el caso del
encadenamiento con cláusulas de Horn.

Resolución

proposicional

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

Resolución

proposicional

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

Cláusulas de Horn

Una cláusula de Horn es una disyunción de literales

que contiene a lo sumo un literal positivo.
Ejemplos: ¬p ∨ ¬q ∨ r , ¬p ∨ ¬r , p

Una cláusula de Horn positiva es una cláusula que

contiene exactamente un literal positivo.

Si contiene otros literales negativos se denomina regla.

Ejemplo: ¬p ∨ ¬q ∨ r .

Si sólo contiene el literal positivo se denomina hecho.

Ejemplo: q.

La regla ¬p ∨ ¬q ∨ r se escribe como



p ∧ q

cuerpo

→ r

cabeza

Un hecho q puede considerarse una regla con cuerpo
vacío,

→ q

Deducción con cláusulas de Horn

Consideraremos un sistema deductivo para trabajar con
cláusulas de Horn positivas.

EA(Σ) es el siguiente sistema deductivo

Axiomas: Un conjunto finito, Σ, de cláusulas de Horn

positivas.

Reglas de inferencia: (A y B son conjunciones de

literales)

I∧ :

A, B
A ∧ B

MP :

A, A → B

B

Resolución

proposicional

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

Deducción con cláusulas de Horn (II)

Se tiene que, para todo hecho, H

Σ |= H ⇐⇒ EA(Σ) H

Además, podemos diseñar un algoritmo de decisión

eficiente para Σ |= H.

Las deducciones en EA(Σ) corresponden al

procedimiento de encadenamiento hacia adelante.

Resolución

proposicional

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

Resolución

proposicional

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

Ejemplo: deducción en EA(Σ)
Veamos que EA(Σ) Q,

[[Hip.]]
[[Hip.]]
[[I∧ aplicada a 1. y 2..]]
[[Hip.]]
[[MP aplicada a 3. y 4.]]
[[I∧: 2. y 5.]]

A
B
A ∧ B
A ∧ B → L
L
B ∧ L
B ∧ L → M [[Hip.]]
L ∧ M

1.
2.
3.
4.
5.
6.
7.
8. M
9.
10. L ∧ M → P [[Hip.]]
11. P
12. P → Q
13. Q

[[MP: 6. y 7.]]
[[I∧: 5. y 8.]]

[[MP: 9. y 10.]]
[[Hip.]]
[[MP: 11. y 12.]]

Σ = {P → Q, L ∧ M → P, B ∧ L → M, A ∧ P → L, A ∧ B → L, A, B}

Procedimiento de encadenamiento hacia adelante

Resolución

proposicional

Un hecho H.
Una enumeración R1, . . . , Rn de los elementos de Σ.

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

Entrada:

Salida:

SI, si EA(Σ) H.
NO, en caso contrario.

Inicialmente, C es el conjunto de todos los hechos que

pertenecen a Σ, j = 1, i = 0.
1. Si H ∈ C , paramos y devolvemos SI.
2. Si j ≤ n y todos los literales del cuerpo de Rj están en

C , entonces
2.1 Si la cabeza de j no está en C se la añadimos a C ,

hacemos j = j + 1, i = 1 y volvemos a 1.

2.2 Si la cabeza de j está en C hacemos j = j + 1 y

volvemos a 2.

3. Si j ≤ n y algún literal del cuerpo de Rj no está en C ,

entonces hacemos j = j + 1 y volvemos a 2.

4. Si j > n y i = 1, hacemos j = 1 y i = 0 y volvemos a 2.
5. Si j > n y i = 0, paramos y devolvemos NO.

Ejemplo: encadenamiento hacia adelante
Veamos que EA(Σ) Q,

Hechos obtenidos

A, B

A, B, L

A, B, L, M

A, B, L, M, P

Reglas usadas
A ∧ B → L

A ∧ B → L, B ∧ L → M

A ∧ B → L, B ∧ L → M, L ∧ M → P

Resolución

proposicional

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

A, B, L, M, P, Q
Σ = {P → Q, L ∧ M → P, B ∧ L → M, A ∧ P → L, A ∧ B → L, A, B}

Σ

Resolución

proposicional

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

La regla de resolución

Generaliza algunas de las reglas de inferencia clásicas:

Modus Ponens :

Modus Tollens :

Encadenamiento :

p,

p → q
q

p → q, ¬q

¬p
p → q,

q → r

p → r

{p},

{¬p, q}
{q}
{¬p, q},

{¬q}

{¬p}

{¬p, q},

{¬q, r}

{¬p, r}

Regla de resolución:

{L1, . . . , L, . . . , Lm,},

{M1, . . . , Lc , . . . , Mk}

{L1, . . . , Lm, M1, . . . , Mk}

Resolución

proposicional

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

Resolución entre cláusulas

Si L ∈ C1 y L ∈ C2 son literales complementarios,
entonces la resolvente de C1 y C2 respecto a L es

resL(C1, C2) = (C1 \ {L}) ∪ (C2 \ {L})

El conjunto de las resolventes de C1 y C2 es:

Res(C1, C2) = {resL(C1, C2) : L ∈ C1 y Lc ∈ C2}.

Ejemplos:

Sea C1 = {p, q,¬r} y C2 = {¬p, r , s}. Entonces

resp(C1, C2) = {q,¬r , r , s}
res¬r (C1, C2) = {p,¬p, q, s}

Resolución

proposicional

Sistemas
deductivos
Pruebas formales
Encadenamiento con
cláusulas de Horn

Resolución
La regla de resolución
Saturación
Estrategias de
resolución

Demostraciones por resolución

Dado un conjunto de cláusulas, S, podemos considerar el
sistema deductivo que tiene a S como conjunto de axiomas y
resolución como única regla de inferencia.

Una demostración por resolución a partir de S es una

sucesión de cláusulas C1, . . . , Cn tal que para cada
i = 1, . . . , n se verifica:

Ci ∈ S, o bien
Existen j, k < i tales que Ci ∈ Res(Cj , Ck ).

Si Cn = diremos que