PDF de programación - Lógica informática (2015–16) - Tema 5: Resolución proposicional

PD Tema 5: Resolución proposicional

Lógica informática (2015–16)
Tema 5: Resolución proposicional

José A. Alonso Jiménez
Andrés Cordón Franco
María J. Hidalgo Doblado

Grupo de Lógica Computacional

Departamento de Ciencias de la Computación e I.A.

Universidad de Sevilla

1 / 37

PD Tema 5: Resolución proposicional

Tema 5: Resolución proposicional

1. Lógica de cláusulas

2. Demostraciones por resolución

3. Algoritmos de resolución

4. Refinamientos de resolución

5. Argumentación por resolución

2 / 37

PD Tema 5: Resolución proposicional

Lógica de cláusulas

Tema 5: Resolución proposicional

1. Lógica de cláusulas

Sintaxis de la lógica clausal
Semántica de la lógica clausal
Equivalencias entre cláusulas y fórmulas
Modelos, consistencia y consecuencia entre cláusulas
Reducción de consecuencia a inconsistencia de cláusulas

2. Demostraciones por resolución

3. Algoritmos de resolución

4. Refinamientos de resolución

5. Argumentación por resolución

3 / 37

PD Tema 5: Resolución proposicional

Lógica de cláusulas

Sintaxis de la lógica clausal

Sintaxis de la lógica clausal

Un átomo es una variable proposicional.

Variables sobre átomos: p, q, r , . . . , p1, p2, . . ..

Un literal es un átomo (p) o la negación de un átomo (¬p).

Variables sobre literales: L, L1, L2, . . ..

Una cláusula es un conjunto finito de literales.

Variables sobre cláusulas: C , C1, C2, . . ..

La cláusula vacía es el conjunto vacío de literales.

La cláusula vacía se representa por .

Conjuntos finitos de cláusulas.

Variables sobre conjuntos finitos de cláusulas: S, S1, S2, . . ..

4 / 37

PD Tema 5: Resolución proposicional

Lógica de cláusulas

Semántica de la lógica clausal

Semántica de la lógica clausal

Una interpretación es una aplicación I : VP → B.
El valor de un literal positivo p en una interpretación I es I(p).
El valor de un literal negativo ¬p en una interpretación I es

I(¬p) =

si I(p) = 0;
si I(p) = 1.

0,

(1,
(1,
(1,

0,

El valor de una cláusula C en una interpretación I es
si existe un L ∈ C tal que I(L) = 1;
en caso contrario.

I(C ) =

0,

El valor de un conjunto de cláusulas S en una interpretación I es

I(S) =

si para toda C ∈ S, I(C ) = 1
en caso contrario.

Prop.: En cualquier interpretación I, I() = 0.

5 / 37

PD Tema 5: Resolución proposicional

Lógica de cláusulas

Equivalencias entre cláusulas y fórmulas

Cláusulas y fórmulas

Equivalencias entre cláusulas y fórmulas

Def.: Una cláusula C y una fórmula F son equivalentes si

I(C ) = I(F ) para cualquier interpretación I.

Def.: Un conjunto de cláusulas S y una fórmula F son

equivalentes si I(S) = I(F ) para cualquier interpretación I.
Def.: Un conjunto de cláusulas S y un conjunto de fórmulas
{F1, . . . , Fn} son equivalentes si, para cualquier interpretación I,
I(S) = 1 syss I es un modelo de {F1, . . . , Fn}.

De cláusulas a fórmulas

Prop.: La cláusula {L1, L2, . . . , Ln} es equivalente a la fórmula
Prop.: El conjunto de cláusulas

L1 ∨ L2 ∨ ··· ∨ Ln.
{{L1,1, . . . , L1,n1}, . . . ,{Lm,1, . . . , Lm,nm}} es equivalente a la
fórmula (L1,1 ∨ ··· ∨ L1,n1) ∧ ··· ∧ (Lm,1 ∨ ··· ∨ Lm,nm ).

6 / 37

PD Tema 5: Resolución proposicional

Lógica de cláusulas

Equivalencias entre cláusulas y fórmulas

De fórmulas a cláusulas (forma clausal)

cláusulas equivalente a F.

Def.: Una forma clausal de una fórmula F es un conjunto de
Prop.: Si (L1,1 ∨ ··· ∨ L1,n1) ∧ ··· ∧ (Lm,1 ∨ ··· ∨ Lm,nm) es una
forma normal conjuntiva de la fórmula F. Entonces, una forma
clausal de F es
{{L1,1, . . . , L1,n1}, . . . ,{Lm,1, . . . , Lm,nm}}.

Ejemplos:

Una forma clausal de ¬(p ∧ (q → r )) es {{¬p, q},{¬p,¬r}}.
Una forma clausal de p → q es {{¬p, q}}.
El conjunto {{¬p, q},{r}} es una forma clausal de las fórmulas

(p → q) ∧ r y ¬¬r ∧ (¬q → ¬p).

Def.: Una forma clausal de un conjunto de fórmulas S es un

Prop.: Si S1, . . . , Sn son formas clausales de F1, . . . , Fn, entonces

conjunto de cláusulas equivalente a S.
S1 ∪ ··· ∪ Sn es una forma clausal de {F1, . . . , Fn}.

7 / 37

PD Tema 5: Resolución proposicional

Lógica de cláusulas

Modelos, consistencia y consecuencia entre cláusulas

Modelos, consistencia y consecuencia entre cláusulas

Def.: Una interpretación I es modelo de un conjunto de cláusulas

S si I(S) = 1.

Ej.: La interpretación I tal que I(p) = I(q) = 1 es un modelo de

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

Def.: Un conjunto de cláusulas es consistente si tiene modelos e

{{¬p, q},{p,¬q}} es consistente.
{{¬p, q},{p,¬q},{p, q},{¬p,¬q}} es inconsistente.

Prop.: Si ∈ S, entonces S es inconsistente.
Def.: S |= C si para todo modelo I de S, I(C ) = 1.

inconsistente, en caso contrario.

Ejemplos:

8 / 37

PD Tema 5: Resolución proposicional

Lógica de cláusulas

Reducción de consecuencia a inconsistencia de cláusulas

Reducción de consecuencia a inconsistencia de cláusulas

Prop: Sean S1, . . . , Sn formas clausales de las fórmulas

F1, . . . , Fn.

{F1, . . . , Fn} es consistente syss S1 ∪ ··· ∪ Sn es consistente.
Si S es una forma clausal de ¬G, entonces son equivalentes

1. {F1, . . . , Fn} |= G.
2. {F1, . . . , Fn¬G} es inconsistente.
3. S1 ∪ ··· ∪ Sn ∪ S es inconsistente.

Ejemplo: {p → q, q → r} |= p → r syss

{{¬p, q},{¬q, r},{p},{¬r}} es inconsistente.

9 / 37

PD Tema 5: Resolución proposicional

Demostraciones por resolución

Tema 5: Resolución proposicional

1. Lógica de cláusulas

2. Demostraciones por resolución

Regla de resolución proposicional
Demostraciones por resolución

3. Algoritmos de resolución

4. Refinamientos de resolución

5. Argumentación por resolución

10 / 37

PD Tema 5: Resolución proposicional

Demostraciones por resolución

Regla de resolución proposicional

Regla de resolución
Reglas habituales:

Modus Ponens:

Modus Tollens:

p → q,
p
q
p → q, ¬q
¬p
p → q,
p → r
Regla de resolución proposicional:
{q1, . . . ,¬r , . . . , qn}
{p1, . . . , pm, q1, , . . . , qn}

{p1, . . . , r , . . . , pm},

Encadenamiento:

q → r

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

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

11 / 37

PD Tema 5: Resolución proposicional

Demostraciones por resolución

Regla de resolución proposicional

Regla de resolución

Def.: Sean C1 una cláusula, L un literal de C1 y C2 una cláusula
que contiene el complementario de L. La resolvente de C1 y C2
respecto de L es

Ejemplos: Resq({p, q},{¬q, r})

ResL(C1, C2) = (C1 {L}) ∪ (C2 {Lc})
= {p, r}
Resq({q,¬p},{p,¬q}) = {p,¬p}
Resp({q,¬p},{p,¬q}) = {q,¬q}
Resp({q,¬p},{q, p})
Resp({p},{¬p})

= {q}
=

Def.: Res(C1, C2) es el conjunto de las resolventes entre C1 y C2
Ejemplos: Res({¬p, q},{p,¬q}) = {{p,¬p},{q,¬q}}

Res({¬p, q},{p, q})
Res({¬p, q},{q, r})
Nota: 6∈ Res({p, q},{¬p,¬q})

= {{q}}
= ∅

12 / 37

PD Tema 5: Resolución proposicional

Demostraciones por resolución

Demostraciones por resolución

Ejemplo de refutación por resolución

Refutación de {{p, q},{¬p, q},{p,¬q},{¬p,¬q}} :

1 {p, q}
Hipótesis
2 {¬p, q}
Hipótesis
3 {p,¬q}
Hipótesis
4 {¬p,¬q} Hipótesis
5 {q}
6 {¬q}
7

Resolvente de 1 y 2
Resolvente de 3 y 4
Resolvente de 5 y 6

13 / 37

PD Tema 5: Resolución proposicional

Demostraciones por resolución

Demostraciones por resolución

Ejemplo de grafo de refutación por resolución

Grafo de refutación de {{p, q},{¬p, q},{p,¬q},{¬p,¬q}} :

14 / 37

PD Tema 5: Resolución proposicional

Demostraciones por resolución

Demostraciones por resolución

Demostraciones por resolución entre cláusulas
Sea S un conjunto de cláusulas.

La sucesión (C1, . . . , Cn) es una demostración por resolución de
la cláusula C a partir de S si C = Cn y para todo i ∈ {1, ..., n} se
verifica una de las siguientes condiciones:

Ci ∈ S;
existen j, k < i tales que Ci es una resolvente de Cj y Ck

La cláusula C es demostrable por resolución a partir de S si

existe una demostración por resolución de C a partir de S. Se
representa por S ‘Res C

Una refutación por resolución de S es una demostración por

resolución de la cláusula vacía a partir de S.

Se dice que S es refutable por resolución si existe una refutación

por resolución a partir de S. Se representa por S ‘Res

15 / 37

PD Tema 5: Resolución proposicional

Demostraciones por resolución

Demostraciones por resolución

Demostraciones por resolución entre fórmulas

Def.: Sean

S1, . . . , Sn formas clausales de las fórmulas F1, . . . , Fn y
S una forma clausal de ¬F
Una demostración por resolución de F a partir de {F1, . . . , Fn} es
una refutación por resolución de S1 ∪ ··· ∪ Sn ∪ S.
{F1, . . . , Fn} si existe una demostración por resolución de F a partir
de {F1, . . . , Fn}. Se representa por {F1, . . . , Fn} ‘Res F.

Def.: La fórmula F es demostrable por resolución a partir de

Ejemplo: {p ∨ q, p ↔ q} ‘Res p ∧ q

1 {p, q}
Hipótesis
2 {¬p, q}
Hipótesis
3 {p,¬q}
Hipótesis
4 {¬p,¬q} Hipótesis
5 {q}
6 {¬q}
7

Resolvente de 1 y 2
Resolvente de 3 y 4
Resolvente de 5 y 6

16 / 37

PD Tema 5: Resolución proposicional

Demostraciones por resolución

Demostraciones por resolución

Adecuación y completitud de la resolución

Prop.: Si C es una resolvente de C1 y C2, entonces {C1, C2} |= C.
Prop.: Si ∈ S, entonces S es inconsistente.
Prop.: Sea S un conjunto de cláusulas.

Prop.: Sean S un conjunto de fórmulas y F es una fórmula.

(Adecuación) Si S ‘Res , entonces S es inconsistente.
(Completitud) Si S es inconsistente, entonces S ‘Res .
(Adecuación) Si S ‘Res F, entonces S |= F.
(Completitud) Si S |= F, entonces