PDF de programación - Verificacióon automática de sistemas de razonamiento

Verificaci´on autom´atica de sistemas de razonamiento∗

(aplicaci´on a la ense˜nanza de la Inteligencia Artificial)

J.L. Ruiz, F.J. Mart´ın, J.A. Alonso, M.J. Hidalgo

Departamento de Ciencias de la Computaci´on e Inteligencia Artificial

Universidad de Sevilla

{jruiz,fjesus,jalonso,mjoseh}@cica.es

Resumen

En este art´ıculo proponemos el uso de sistemas
de demostraci´on autom´atica como herramienta
pr´actica en la ense˜nanza de las asignaturas de
Ciencias de la Computaci´on e Inteligencia Arti-
ficial. Esta propuesta se ilustra con un ejemplo:
la verificaci´on de la correcci´on y completitud de
un peque˜no sistema de demostraci´on autom´atica
de f´ormulas proposicionales. Para ello usamos
el demostrador de Boyer y Moore.

1 Introducci´on

Uno de los usos principales de los sistemas de
deducci´on y verificaci´on autom´atica de teoremas
es el razonamiento sobre propiedades de progra-
mas. Es decir, dado un programa, se formali-
zan las propiedades que se le suponen, en forma
de teoremas; la veracidad de esos teoremas se
comprueba mediante un sistema de razonamien-
to autom´atico. El programa se convierte as´ı en
un objeto sobre el que razonar. Varios son los
objetivos que se consiguen:
• En primer lugar, se formalizan las propie-
dades esperadas de un algoritmo, con lo que
queda mucho m´as clara la estructura l´ogica
del mismo.

• Las pruebas sobre propiedades de progra-
mas suelen ser mucho m´as largas y pe-
sadas que las de resultados matem´aticos.
Es especialmente conveniente el tratarlas
mec´anicamente.

• Por otro lado, supone un proceso efectivo de
asegurar la correcci´on y otras propiedades
de los programas.

∗Este trabajo ha sido financiado por la DGES del

MEC, proyectos PB96-0098-C04-04 y PB96-1345

Esta verificaci´on autom´atica de teoremas pue-
de ser utilizada para la prueba de propiedades
de algoritmos dentro del campo de la Inteligen-
cia Artificial, incluso dentro del propio campo
del Razonamiento Autom´atico.

En este art´ıculo proponemos la verificaci´on
autom´atica como instrumento en la ense˜nanza
de la Inteligencia Artificial, disponiendo as´ı de
una herramienta para dar rigor y razonar sobre
algunas de sus t´ecnicas m´as conocidas, ayudan-
do a una comprensi´on m´as profunda de la ma-
teria.

Como ejemplo, planteamos la verificaci´on au-
tom´atica de la correcci´on y completitud de un
demostrador de f´ormulas en l´ogica proposicio-
nal. La verificaci´on se realiza usando el demos-
trador de Boyer y Moore.

2 El demostrador de Boyer y

Moore.

El demostrador de Boyer y Moore, tambi´en co-
nocido como NQTHM, implementa una l´ogica
computacional, cuya principal caracter´ıstica es
la automatizaci´on del principio de inducci´on,
que lo hace especialmente adecuado para la de-
mostraci´on de propiedades de programas. Una
impresionante lista de teoremas han sido proba-
dos y verificados en NQTHM, en el campo de
las matem´aticas, el software y el hardware. Una
detallada informaci´on del sistema se puede en-
contrar en [?] y [?].

2.1 La l´ogica computacional.

Hacemos aqu´ı una breve descripci´on de la l´ogica
que usa el demostrador de Boyer y Moore (lla-
mada l´ogica computacional) para formalizar y
demostrar teoremas. Se trata de un fragmento

de la l´ogica de primer orden, sin cuantificadores.
Su sintaxis y sem´antica est´a basada en el len-
guaje Lisp. Por tanto, usa una notaci´on prefija
para denotar t´erminos. Por ejemplo, escribimos
(and p q) en lugar de p ∧ q.

Incluye la l´ogica proposicional, variables,
s´ımbolos de funci´on y el predicado de igualdad.
Adem´as de las conectivas usuales (AND, OR, NOT,
IMPLIES), se incluye la conectiva IF (la funci´on
if-then-else).

La l´ogica incluye inicialmente la definici´on de
los n´umeros naturales y de los pares ordenados,
como objetos construidos recursivamente:

• Los naturales, obtenidos a partir del obje-
to base (ZERO) y del constructor ADD1 (la
funci´on sucesor). Su funci´on de acceso (des-
tructor) es SUB1.

• Los pares ordenados, obtenidos a partir del
constructor CONS, con los destructores CAR
y CDR.

El usuario puede definir nuevos tipos de datos,
dando nuevos objetos base, constructores y des-
tructores. Esto har´a que nuevos axiomas, des-
cribiendo al nuevo tipo de dato, se a˜nadan a la
l´ogica. La caracter´ıstica principal de estos tipos
de datos definidos por el usuario es que pueden
estar definidos recursivamente. Esto es especial-
mente ´util, ya que la mayor´ıa de las propiedades
de los programas se prueban por inducci´on en la
estructura de los datos que reciben como entra-
da.

Si se quiere que el demostrador verifique pro-
piedades de algoritmos, ´estos se tienen que po-
der definir dentro de la l´ogica. Esto se consigue
mediante el uso de funciones al estilo LISP. Por
ejemplo, podr´ıamos definir un algoritmo de con-
catenaci´on de listas de la siguiente manera:

(defn conc (l1 l2)

(if (not (listp l1))

l2

(cons (car l1)

(conc (cdr l1) l2))))

S´olo se admite la definici´on de una funci´on
despu´es de que el demostrador haya sido capaz
de probar que es total (principio de definici´on).
Esto asegura la consistencia de la l´ogica. La
prueba de que una funci´on es total consiste en
ver que sus argumentos decrecen en cada llama-
da recursiva, respecto de una determinada “me-
dida”, que se supone bien fundamentada.

Adem´as de las reglas de inferencia de la l´ogica
proposicional, de la igualdad, y la instanciaci´on,
la l´ogica incluye un principio de inducci´on ma-
tem´atica. Este principio, en esencia, asegura que
para demostrar que una propiedad es cierta pa-
ra un determinado objeto, podemos suponer que
es cierta para objetos m´as peque˜nos (respecto a
cierta “medida” bien fundamentada).

Existe una dualidad entre los principios de de-
finici´on y de inducci´on, de manera que argumen-
tos similares a los usados en la prueba de la ad-
misi´on de la definici´on de una funci´on, pueden
servir para probar por inducci´on determinadas
propiedades de la misma.

2.2 El demostrador.

El usuario puede pedir al sistema que intente
la prueba de un determinado teorema expresa-
do con el lenguaje de la l´ogica computacional.
Por ejemplo, para intentar demostrar que la fun-
ci´on que concatena listas (que hemos definido
anteriormente) es asociativa, escribiriamos la si-
guiente expresi´on:

(prove-lemma asociatividad-conc (rewrite)

(equal (conc x (conc y z))

(conc (conc x y) z)))

Esto hace que el sistema aplique una serie de
t´ecnicas encaminadas a encontrar una prueba
del teorema requerido. Si el sistema lo consigue,
es posible reconstruir una prueba del teorema
usando los axiomas y esquemas de inferencia de
la l´ogica anteriormente referida. Adem´as, el re-
sultado puede ser usado en posteriores pruebas.
Si el sistema falla en el intento, nada podemos
asegurar sobre la validez del teorema.

La principal t´ecnica usada es la de simplifi-
caci´on, cuyo componente b´asico es un sistema
de reglas de reescritura, obtenidas a partir de
resultados anteriores.

La segunda t´ecnica en importancia consiste
en aplicar el principio de inducci´on. Presenta
la dificultad de tener que escoger un esquema
de inducci´on adecuado para la prueba. Una de
las principales aportaciones del sistema de B. &
M. es la de obtener esos esquemas de manera
mec´anica, mediante una serie de heur´ısticas.

Otras t´ecnicas se pueden aplicar tambi´en a
una f´ormula como parte del intento de probar
que es teorema: generalizaci´on, eliminaci´on de
irrelevancias, eliminaci´on de destructores, etc.

2.3 El papel del usuario.

Aunque, en sentido estricto, NQTHM no es in-
teractivo, de alguna manera, el usuario puede
influir en la b´usqueda de una demostraci´on.

Si un resultado se ha demostrado previamen-
te, ´este puede ser usado por el demostrador en la
prueba de posteriores resultados. La manera en
que el sistema usa estos teoremas previos, es, ge-
neralmente, almacen´andolos en forma de reglas
de simplificaci´on. Por ejemplo, una vez probada
la asociatividad de conc, podremos usarla en in-
tentos de prueba posteriores para reescribir una
expresi´on de la forma (conc X (conc Y Z)) co-
mo (conc (conc X Y) Z).

Usualmente, el sistema es incapaz de probar
un resultado de una cierta complejidad sin nin-
guna informaci´on adicional, a´un cuando se trate
de un teorema demostrable en la l´ogica del sis-
tema.

El proceso t´ıpico que se sigue en un intento

de demostraci´on es el siguiente:

• El usuario conoce una prueba a mano de un

resultado y quiere verificarla.

• Formaliza el resultado en la l´ogica del sis-

tema.

• Gu´ıa al demostrador hacia la prueba cono-

cida, demostrando lemas previos.

• Usualmente, en primera instancia, la prue-
ba de un teorema por parte del sistema sue-
le fallar (a no ser que sea muy “simple”).
Inspeccionando esta prueba fallida es posi-
ble obtener como consecuencia que se ne-
cesitan una serie de lemas que han de ser
probados previamente.

Como resultado final la prueba de un teorema
consiste en una serie de lemas que van aportan-
do al sistema el conocimiento suficiente como
para permitirle completar la prueba del resulta-
do principal.

3 Verificaci´on de un sistema de
demostraci´on proposicional.

3.1 Introducci´on.

Presentamos en esta secci´on un ejemplo muy
ilustrativo del uso de NQTHM en la demostra-
ci´on de propiedades de un algoritmo, basado en

un ejemplo presentado en [?]. Se trata de defi-
nir un algoritmo que decide si una f´ormula de
la l´ogica proposicional es tautolog´ıa. Est´a ba-
sado en la t´ecnica conocida como Diagramas de
Decisi´on Binaria (BDDs), ver [?]. La idea prin-
cipal consiste en transformar la f´ormula a otra
cuya ´unica conectiva sea if-then-else y que s´olo
tenga ´atomos en el test. Es sobre estas f´ormulas
normalizadas donde se decide la propiedad de
ser tautolog´ıa. Usaremos NQTHM para probar
la correcci´on y completitud de este demostrador
de tautolog´ıas.

Varias son las caracter´ısticas que hacen espe-
cialmente interesante el ejemplo planteado des-
de el punto de vista docente. Cualquier sis-
tema l´ogico tiene como una de sus componen-