PDF de programación - Tema 2: Procedimiento general de demostración

Demostración automática de teoremas

Curso 2002–03

Tema 2: Procedimiento general

de demostración

José A. Alonso Jiménez
Joaquín Borrego Díaz

Antonia Chávez González

Dpto. de Ciencias de la Computación e Inteligencia Artificial

Universidad de Sevilla

DAT 2002–03

CcIa

Procedimiento general de demostración

2.1

Razonamiento proposicional con OTTER
x Base de conocimiento
u Base de reglas:

* R1: Si el animal tiene pelos es mamífero.
* R2: Si el animal da leche es mamífero.
* R3: Si el animal es un mamífero y tiene pezuñas es ungulado.
* R4: Si el animal es un mamífero y rumia es ungulado.
* R5: Si el animal es un ungulado y tiene cuello largo es una jirafa.
* R6: Si el animal es un ungulado y tiene rayas negras es una cebra.

u Base de hechos:

* H1: El animal tiene pelos.
* H2: El animal tiene pezuñas.
* H3: El animal tiene rayas negras.

u Consecuencia

* El animal es una cebra.

DAT 2002–03

CcIa

Procedimiento general de demostración

2.2

Razonamiento proposicional con OTTER
x Representación en OTTER (animales.in)

formula_list(sos).
tiene_pelos | da_leche -> es_mamifero.
es_mamifero & (tiene_pezuñas | rumia) -> es_ungulado.
es_ungulado & tiene_cuello_largo -> es_jirafa.
es_ungulado & tiene_rayas_negras -> es_cebra.

% Reglas 1 y 2
% Reglas 3 y 4
% Regla 5
% Regla 6

tiene_pelos & tiene_pezuñas & tiene_rayas_negras.

% Hechos 1, 2 y 3

-es_cebra.
end_of_list.

% -Conclusión

set(binary_res).
set(very_verbose).

% Regla de inferencia: Resolución binaria
% Da mucha información sobre generación de cláusulas.

x Procesamiento con OTTER

otter <animales.in >animales.out

DAT 2002–03

CcIa

Procedimiento general de demostración

2.3

Razonamiento proposicional con OTTER
x Transformación a cláusulas

-------> sos clausifies to:
list(sos).
1 [] -tiene_pelos | es_mamifero.
2 [] -da_leche | es_mamifero.
3 [] -es_mamifero | -tiene_pezuñas | es_ungulado.
4 [] -es_mamifero | -rumia | es_ungulado.
5 [] -es_ungulado | -tiene_cuello_largo | es_jirafa.
6 [] -es_ungulado | -tiene_rayas_negras | es_cebra.
7 [] tiene_pelos.
8 [] tiene_pezuñas.
9 [] tiene_rayas_negras.
10 [] -es_cebra.
end_of_list.

x Cláusulas
u Definiciones:

• Una cláusula es una disyunción de literales.
• Un literal es un átomo o la negación de un átomo.

DAT 2002–03

CcIa

Procedimiento general de demostración

2.4

Razonamiento proposicional con OTTER
u Procedimiento de transformación a cláusulas:

1. Eliminar las equivalencias usando la relación

A ↔ B ≡ (A → B) ∧ (B → A)

2. Eliminar las implicaciones usando la equivalencia

A → B ≡ ¬A ∨ B

3. Interiorizar las negaciones usando las equivalencias

¬(A ∧ B) ≡ ¬A ∨ ¬B
¬(A ∨ B) ≡ ¬A ∧ ¬B
¬¬A ≡ A

(1)

(2)

(3)
(4)
(5)

4. Interiorizar las disyunciones usando la propiedad distributiva de la disyunción

sobre la conjunción

A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C)
(A ∧ B) ∨ C ≡ (A ∨ C) ∧ (B ∨ C)

(6)
(7)

DAT 2002–03

CcIa

Procedimiento general de demostración

2.5

Razonamiento proposicional con OTTER
x Reglas dependientes

set(binary_res).

dependent: set(factor).
dependent: set(unit_deletion).

x Búsqueda de la prueba

=========== start of search ===========

given clause #1: (wt=1) 7 [] tiene_pelos.

given clause #2: (wt=1) 8 [] tiene_pezugnas.

given clause #3: (wt=1) 9 [] tiene_rayas_negras.

given clause #4: (wt=1) 10 [] -es_cebra.

DAT 2002–03

CcIa

Procedimiento general de demostración

2.6

Razonamiento proposicional con OTTER

given clause #5: (wt=2) 1 [] -tiene_pelos|es_mamifero.

0 [binary,1.1,7.1] es_mamifero.

** KEPT (pick-wt=1): 11 [binary,1.1,7.1] es_mamifero.
11 back subsumes 2.
11 back subsumes 1.

given clause #6: (wt=1) 11 [binary,1.1,7.1] es_mamifero.

given clause #7: (wt=3) 3 [] -es_mamifero| -tiene_pezugnas|es_ungulado.

0 [binary,3.1,11.1] -tiene_pezugnas|es_ungulado.

** KEPT (pick-wt=1): 12 [binary,3.1,11.1,unit_del,8] es_ungulado.

0 [binary,3.2,8.1] -es_mamifero|es_ungulado.
Subsumed by 12.

12 back subsumes 4.
12 back subsumes 3.

DAT 2002–03

CcIa

Procedimiento general de demostración

2.7

Razonamiento proposicional con OTTER

given clause #8: (wt=1) 12 [binary,3.1,11.1,unit_del,8] es_ungulado.

given clause #9: (wt=3) 5 [] -es_ungulado| -tiene_cuello_largo|es_jirafa.

0 [binary,5.1,12.1] -tiene_cuello_largo|es_jirafa.

** KEPT (pick-wt=2): 13 [binary,5.1,12.1] -tiene_cuello_largo|es_jirafa.
13 back subsumes 5.

given clause #10: (wt=2) 13 [binary,5.1,12.1] -tiene_cuello_largo|es_jirafa.

given clause #11: (wt=3) 6 [] -es_ungulado| -tiene_rayas_negras|es_cebra.

0 [binary,6.1,12.1] -tiene_rayas_negras|es_cebra.

** KEPT (pick-wt=0): 14 [binary,6.1,12.1,unit_del,9,10] $F.

-----> EMPTY CLAUSE at

0.00 sec ----> 14 [binary,6.1,12.1,unit_del,9,10] $F.

DAT 2002–03

CcIa

Procedimiento general de demostración

2.8

Razonamiento proposicional con OTTER
x Demostración

Length of proof is 2. Level of proof is 2.

---------------- PROOF ----------------

1 [] -tiene_pelos|es_mamifero.
3 [] -es_mamifero| -tiene_pezugnas|es_ungulado.
6 [] -es_ungulado| -tiene_rayas_negras|es_cebra.
7 [] tiene_pelos.
8 [] tiene_pezugnas.
9 [] tiene_rayas_negras.
10 [] -es_cebra.
11 [binary,1.1,7.1] es_mamifero.
12 [binary,3.1,11.1,unit_del,8] es_ungulado.
14 [binary,6.1,12.1,unit_del,9,10] $F.

------------ end of proof -------------

Search stopped by max_proofs option.

DAT 2002–03

CcIa

Procedimiento general de demostración

2.9

Razonamiento proposicional con OTTER
x Estadísticas

-------------- statistics -------------
clauses given
clauses generated

binary_res generated
factors generated

clauses forward subsumed

(subsumed by sos)

unit deletions
clauses kept
empty clauses
clauses back subsumed
usable size

11
5
5
0
1
1
4
3
1
5
8

----------- times (seconds) -----------
user CPU time
system CPU time

0.00
0.01

(0 hr, 0 min, 0 sec)
(0 hr, 0 min, 0 sec)

DAT 2002–03

CcIa

Procedimiento general de demostración

2.10

Razonamiento proposicional con OTTER
x Cláusulas usadas

1 [] -tiene_pelos | es_mamifero.
2 [] -da_leche | es_mamifero.
3 [] -es_mamifero | -tiene_pezugnas |es_ungulado.
4 [] -es_mamifero | -rumia | es_ungulado.
5 [] -es_ungulado | -tiene_cuello_largo | es_jirafa.
6 [] -es_ungulado | -tiene_rayas_negras |es_cebra.
7 [] tiene_pelos.
8 [] tiene_pezugnas.
9 [] tiene_rayas_negras.

10 [] -es_cebra.
11 [binary,1.1,7.1] es_mamifero.
12 [binary,3.1,11.1,unit_del,8] es_ungulado.
13 [binary,5.1,12.1] -tiene_cuello_largo|es_jirafa.
14 [binary,6.1,12.1,unit_del,9,10] $F.

DAT 2002–03

CcIa

Procedimiento general de demostración

2.11

Razonamiento proposicional con OTTER
x Evolución del soporte y usable

| Usable

+----+----------------------+---------------------+
| N | Soporte
|
+----+----------------------+---------------------+
| 0 | 1 2 3 4 5 6 7 8 9 10 |
|
|
| 1 | 1 2 3 4 5 6 8 9 10
| 7
|
| 2 | 1 2 3 4 5 6 9 10
| 8 7
| 3 | 1 2 3 4 5 6 10
|
| 9 8 7
|
| 4 | 1 2 3 4 5 6
| 10 9 8 7
| 5 | 3 4 5 6 11
|
| 10 9 8 7
|
| 6 | 3 4 5 6
| 11 10 9 8 7
|
| 7 | 5 6 12
| 11 10 9 8 7
| 8 | 5 6
|
| 12 11 10 9 8 7
|
| 9 | 6 13
| 12 11 10 9 8 7
| 10 | 6
|
| 13 12 11 10 9 8 7
| 11 | 14
| 6 13 12 11 10 9 8 7 |
+----+----------------------+---------------------+

DAT 2002–03

CcIa

Procedimiento general de demostración

2.12

Razonamiento proposicional con OTTER
x Procedimiento de búsqueda de pruebas

Mientras el soporte es no vacío y no se ha encontrado una refutación

1. Seleccionar como cláusula actual la cláusula menos pesada del soporte;
2. Mover la cláusula actual del soporte a usable;
3. Calcular las resolventes de la cláusula actual con las cláusulas usables.
4. Procesar cada una de las resolventes calculadas anteriormente.
5. Añadir al soporte cada una de las cláusulas procesadas que supere

el procesamiento.

DAT 2002–03

CcIa

Procedimiento general de demostración

2.13

Razonamiento proposicional con OTTER

El procesamiento de cada una de resolventes consta de los siguientes pasos
(los indicados con * son opcionales):

* 1. Escribir la resolvente.
* 2. Aplicar a la resolvente eliminación unitaria (i.e. elimina los literales

de la resolvente tales que hay una cláusula unitaria complementaria en
usable o en soporte).

3. Descartar la resolvente y salir si la resolvente es una tautología.
4. Descartar la resolvente y salir si la resolvente es subsumida por alguna

cláusula de usable o del soporte (subsunción hacia adelante).

5. Añadir la resolvente al soporte.
* 6. Escribir la resolvente retenida.

7. Si la resolvente tiene 0 literales, se ha encontrado una refutación.
8. Si la resolvente tiene 1 literal, entonces buscar su complementaria

(refutación) en usable y soporte.

* 9. Escribir la demostración si se ha encontrado una refutación.
-------------
* 10. Descartar cada cláusula de usable o del soporte subsumida por la

resolvente (subsunción hacia atrás).

El paso 10 no se da hasta que los pasos 1-9 se han aplicado a todas las
resolventes.

DAT 2002–03

CcIa

Procedimiento general de demostración

2.14

Razonamiento proposicional con OTTER (II)
x Redistribución del soporte (animales 2.in)

formula_list(usable).
tiene_pelos | da_leche -> es_mamifero.
es_mamifero & (tiene_pezuñas | rumia) -> es_ungulado.
es_ungulado & tiene_cuello_largo -> es_jirafa.
es_ungulado & tiene_rayas_negras -> es_cebra.

% Reglas 1 y 2
% Reglas 3 y 4
% Regla 5
% Regla 6

tiene_pelos & tiene_pezuñas & tiene_rayas_negras.
end_of_list.

% Hechos 1, 2 y 3

formula_list(sos).
-es_cebra.
end_of_list.

% -Conclusión

set(binary_res).
set(very_verbose).

% Regla de inferencia: resolución binaria.
% Da mucha información sobre generación de cláusulas.

x Procesamiento con OTTER

otter <animales_2.in >animales_2.out

DAT 2002–03

CcIa

Procedimiento general de demostración

2.15

Razonamiento proposicional con OTTER (II)
x Transformación a cláusulas

-------> usable clausifies to:
list(usable).
1 [] -tiene_pelos|es_mamifero.
2 [] -da_leche|es_mamifero.
3 [] -es_mamifero| -tiene_pezugnas|es_ungulado.
4 [] -es_mamifero| -rumia|es_