PDF de programación - Tesis: Guillermo Ita - METODO RM PARA LA DEMOSTRACION AUTOMATICA DE TEOREMAS

CENTRO TP i K Y E O T W li S Y C I

F -,T '; 's ■' V A NZ A DOS DEL

i. P. N.

l

i

b

i

b


INGENIERIA ELECTRICA

o

t

e

c

a

CENTRO DE INVESTIGACION Y DE ESTUDIOS AVANZADOS

DEL

INSTITUTO POLITECNICO NACIONAL

DEPARTAMENTO DE INGENIERIA ELECTRICA

SECCION DE COMPUTACION

C E N T R O L '

-7 Í : ; í v í

. ■

E S T U D IO S M '.W .Z a D O S d :

I. P . N .

i

B I B L I O T E C A
INGENIERIA ELECTRICA

" METODO RM PARA LA DEMOSTRACION

AUTOMATICA DE TEOREMAS M

Tesis que presenta el Lic. en Computación Guillermo De Ita

Luna para obtener el grado de MAESTRO EN CIENCIAS en la especiali­

dad de Ingeniería Eléctrica. Trabajo dirigido por el Dr. Guillermo

Morales Luna.

Becario del CONACYT

México D.F., Abril de 1989

A MIS PADRES

Sr. José De Ita Pérez
Sra. Judith Luna Soto

Al pensamiento tenaz, lucha constante, ejemplo invaluable de
fe y trabajo. Con respeto y amor a quien dirigió mis primeros
pensamientos y fortaleció mi espíritu. A ti madre.

CFNTno rv; w y e s v .g * :^.í v
E S T U C O S A V A K ZA D C 3 D U

i

b

a
b
INGENIERIA ELECTRICA

c

i

i. P. N.

l

o

t

e

A MIS HERMANOS

Compañeros fraternales que siempre me han apoyado. Con cariño

a Ustedes que han sido mis grandes amigos.

CENTRO DE I N V E S T I V.’X V 3S

ESTUDIOS A V A N Z A D O S DEL

L P. N.

B I B L I O T E C A
INGENIERIA ELECTRICA

Expreso mi agradecimiento al asesor: Dr. Guillermo Morales

Luna, por su contribución, por dirigir, alentar, apoyar y revisar
este trabajo. Sus comentarios fueron una ayuda inapreciable en el
desarrollo del mismo. Agradezco la ayuda brindada por los profeso­
res: Dr. Josef Kolar y al Dr. Ernesto López que aparte de los
consejos en la elaboración del trabajo hicieron una valiosa
revisión de su documentación.
Igualmente agradezco la ayuda brindada por mi compañera: Rosario
Varela Hernández cuya motivación y comprensión del trabajo, me
motivó y auxilió para la terminación del mismo.
Extiendo mi agradecimiento a los profesores y compañeros de la
sección de computación del CINVESTAV, quienes permitieron una
atmósfera intelectual agradable y rica en experiencias para su
desarrollo. Este trabajo fué auspiciado por la beca número 54414
del Consejo Nacional de Ciencia y Tecnología (CONACYT).

C E N T R O D E I N V E S T I S * CI QR Y 6 c

E S T U D I O S A V A N Z A D O S í'íl

I. P . N .

B I B L I O T E C A
INGENIERÍA ELECTRICA

INDICE

INTRODUCCION

I) PRELIMINARES

1.1) CALCULO DE PROPOSICIONES
1.2) CALCULO DE PREDICADOS
1.3) REPRESENTACION CLAUSULAR
1.4) DEMOSTRACION POR REFUTACION
1.5) PROCEDIMIENTO DE UNIFICACION
1.6) INDECIBILIDAD DEL CALCULO DE PREDICADOS

II) METODO RM PARA LA DEMOSTRACION AUTOMATICA DE TEOREMAS
2.1) FUNDAMENTOS TEORICOS
2.2) TRATAMIENTOS CLASICOS
2.3) METODO DE REDUCCION MATRICIAL (METODO RM)

III) EXPLICACION DETALLADA DEL METODO RM
3.1) ESTRATEGIAS UTILIZADAS EN EL METODO RM
3.2) ESTRUCTURA DE DATOS UTILIZADA EN LA CONSTRUCCION

DEL METODO RM.

3.3) ALGORITMO LOGICO Y DE CONTROL

IV) CONCLUSIONES

BIBLIOGRAFIA

APENDICE

A)

MANUAL DE USO Y UNA SESION CON EL PROGRAMA

Página

1

3
3
5
7
9
9
10

12
12
14
18

22
22
25

28

32

35

37

INTRODUCCION

Una de las más grandes ambiciones en la ciencia, ha sido la
de encontrar un procedimiento general de decisión para la prueba
de teoremas. Aunque tal deseo data desde Leibniz (1646-1716), esto
no fue formalizado sino hasta principios del siglo XX, en que
David Hilbert planteó a la comunidad matemática el construir un
sistema formal general, completo y consistente para realizar
correctamente (de acuerdo a las reglas del sistema) toda
demostración matemática.

Un procedimiento que se convirtió en fundamental fué dado por
Jacques Herbrand (1930), como un método mecánico para la prueba de
teoremas, aunque tal procedimiento era muy ineficiente en la prác­
tica. Pero no fué hasta que Kurt Godel (1936) reveló la imposibi­
lidad de construir un sistema formal (axiomático) completo y
consistente en el cual puedan demostrarse todas las verdades mate­
máticas. Aún con tales limitaciones la Demostración Automática de
Teoremas, una de las ramas en
la Inteligencia Artificial, se
mantuvo en investigación, hasta que en la década de los 6 0 ’s un
creciente interés es puesto en ella, propiciado por la aplicación
de la computación en las técnicas de demostración, que da como
resultado la creación de diversos métodos como son: Davis y Putnam
(1960), Gilmore (1960), Loveland (1962), Davis y Hinman (1964).
Robinson (1965), Prawitz (1969).

En la actualidad, las técnicas utilizadas en la Demostración

Automática de Teoremas, se aplican a muchas áreas, tales como:
- El análisis,

síntesis y verificación de programas por

computadora.

- Los sistemas deductivos de respuestas a preguntas.
- Los sistemas de planeación.
- Los sistemas expertos.
- El modelado para el razonamiento del sentido común.
- Como base para los lenguajes de programación lógica.
Y el número de aplicaciones va en aumento.

El objetivo del método desarrollado en este trabajo de tesis,

es el de diseñar y construir un procedimiento general original que
realice eficientemente(igual o mejor que los métodos ya conocidos)
la prueba de teoremas en el cálculo de predicados.
Como es sabido, el procedimiento inicial dado por Herbrand
es
ineficiente en la práctica, ya que se basa en la generación de una
sucesión de conjuntos

... con instancias básicas del

conjunto cláusular inicial S. Tal sucesión
principio no se sabe para cual valor de N, puede probarse
la
inconsistencia de S^. Con el fin de agilizar la búsqueda del S^,

puede ser infinita y en

Davis y Putnam adicionaron cuatro reglas que simplifican la prueba
para la inconsistencia de S^.

Con el fin de evitar la generación de tal sucesión, dos técnicas
principales han sido propuestas: una es el principio de Resolución
de Robinson y otra el método propuesto por Prawitz.

1

Sin embargo, el autor considera que estas dos últimas técnicas no
son excluyentes y por el contrario, evitando las incoveniencias
inherentes a cada una de ellas y aprovechando las ventajas de
ambas, las ideas principales en estas técnicas fueron combinadas
en un modelo basado en reglas, con un orden parecido al de las
reglas en el método de Davis y Putnam. Esto forma la base del
método diseñado por el autor denominado METODO RM.

El interés por realizar este trabajo puede remontarse a la
formación tenida por el autor en la carrera de ’Licenciado en
Computación’ realizada en la E.C.F.M. de la Universidad Autónoma
de Puebla, en particular a los cursos de Lógica Computacional cur­
sados tanto en esta escuela como en el CINVESTAV - I.P.N. , en
donde además se efectuaron proyectos en los que se programaron
algunos de los métodos ya conocidos en la Demostración Automática
de Teoremas.

En el capítulo I de este documento de tesis, se dan los
fundamentos teóricos necesarios para la comprensión de la teoría
en la que se sustentan los métodos de demostración. También se
explican algunos de los elementos a utilizar por el método RM.

En el capítulo II se presenta el procedimiento de Herbrand,

se explica tanto el método RM como los métodos en los que se basa.

En el capítulo III se describe a detalle al método RM, se
explican los diversos módulos que lo componen; las estrategias que
utiliza, el algoritmo lógico y de control y la estructura de datos
usada para su implementación en el lenguaje LISP.

Por último, en las conclusiones se mencionan los objetivos
alcanzados, los conocimientos y experiencias adquiridas, las
limitaciones encontradas al trabajo y se mencionan algunas de las
posibles aplicaciones y/o extensiones a éste trabajo.

El apéndice A, guía a los futuros usuarios del programa.
Indica tanto como ejecutarlo, así como la sintaxis a seguir al
introducir los datos de entrada. Señala el formato y el tipo de
resultados que se debe esperar. Y por último se ejemplifica una
sesión con el programa.

2

PRELIMINARES

Los procesos del pensamiento han sido objeto de estudio de
varias ciencias, una de ellas que desde sus inicios trató de
formalizar los procesos intelectivos del razonamiento es la Lógi­
ca. Se dice que la capacidad de razonar es la que distingue al ser
humano de otras especies, resulta paradójico entonces,
el querer
mecanizar ’e s o ’ que es lo más humano que se tiene. Sin embargo, ya
los griegos sabían que el razonamiento es un proceso sujeto a
esquemas y que en parte está gobernado por leyes perfectamemte
formulables. Aristóteles formalizó los silogismos y Euclides la
geometría.

En el siglo XIX los lógicos ingleses George Boole y August De
Morgan sometieron los esquemas estrictamente deductivos del razo­
namiento a una formalización que deja muy atrás la formalización
Aristotélica. Gottlob Frege y Giuseppe Peano se dieron a la tarea
de combinar el razonamiento formai con el estudio de conjuntos y
números. En Gotinga, Alemania, David Hilbert elaborò formaiizacio-
nes de geometrías más estrictas