Algoritmo de Hao Wang (prolog)

Una de mis prácticas de programación en análisis lógico fue implementar el algoritmo de Hao Wang en prolog. Es decir implementar un demostrador de teoremas. Ahora en uno de los grupos del cual soy ayudante les dejaron implementar ese algoritmo. Una descripción del algoritmo la pueden encontrar aqui. Pongo mi implementación de aquellos días (planeo mejorarlo un día de estos); obviamente como todo lo que programaba en mis años de juventud no es eficiente ni elegante. De hecho hay teoremas para los cuales tarda en responder... mucho tiempo, en verdad mucho...

Para probar el programa:

1.Cargar el programa
2. introducir el teorema

Es decir:

page@page ~]$ pl
Welcome to SWI-Prolog (Multi-threaded, 32 bits, Version 5.6.64)
Copyright (c) 1990-2008 University of Amsterdam.
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software,
and you are welcome to redistribute it under certain conditions.
Please visit http://www.swi-prolog.org for details.

For help, use ?- help(Topic). or ?- apropos(Word).

?- [haoWang].


?- wang([-p,-q -> r&p],[q,s&r]).
true ;

?- wang([p#r],[p]).
false.

?- wang([p&r -> -q&s, p,r],[s]).
true ;

El guion (-) representa la negación, el (&) la conjunción, el # la disyunción, -> es la implicación, <-> el bicondicional. El conjunto de premisas es la primer lista, la segunda lista es el teorema.

Repito: en mis dias de juventud sólo me interesaba sacar los programas por lo que éstos pueden ser no eficientes y nada elegantes (hoy revisandolo le encontré una infinidad de tonterias... y mucha basura... pero total). Si alguien mejora el programa pues que lo pase. Para descargar el programa Aqui.