Improved resolution theorem prover (RTP v. 1.11)

[Update: March 26th 2017: small tweak for incremental release RTP v. 1.11. The change is to the order of new goals in 'binary-resolve', which adopts a faster-converging pure depth-first search. See the READ-ME file for details.]

===

You will have previously seen the announcement about the first (tutorial) version of my resolution theorem prover in Lisp.

Today I'm releasing version 1.1 which is easier to use and gives a clearer output.

Below are the "Who does Lady Sally Fowler like?" proofs (compare with the previous version).

The code is available at the AI code in Lisp Resource on the right of your (web view) screen.

Or follow these links for the program file and genealogical test data.

Retrieve program file: RTP-v1.11 and test-data:  Genealogical-etc-test-data.


---    To determine (likes sally ?who)    ---

 > (prove-it *g-mge1* *mge-axioms* 8)

Do you want to see all the proof steps y/n?  n

Conclusion = ((<- ((LIKES SALLY SALLY))))

(13)   ((LIKES ?X ?X) <-)
(14)   (<- ((LIKES SALLY ?WHO)))
(19 14 13)   +EMPTY-CLAUSE+
--------------------------------------

Conclusion = ((<- ((LIKES SALLY ROD))))

(5)   ((LIKES SALLY ROD) <-)
(14)   (<- ((LIKES SALLY ?WHO)))
(16 14 5)   +EMPTY-CLAUSE+
--------------------------------------

Conclusion = ((<- ((LIKES SALLY RENNER))))

(4)   ((LIKES SALLY RENNER) <-)
(14)   (<- ((LIKES SALLY ?WHO)))
(15 14 4)   +EMPTY-CLAUSE+
--------------------------------------

Conclusion = ((<- ((LIKES SALLY MOTIES))))

(13)   ((LIKES ?X ?X) <-)
(10)   ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES)))
(14)   (<- ((LIKES SALLY ?WHO)))
(17 14 10)   (<- ((LIKES ?WHO MOTIES)))
(24 17 13)   +EMPTY-CLAUSE+
--------------------------------------

Conclusion = ((<- ((LIKES SALLY HORVATH))))

(9)   ((LIKES HORVATH MOTIES) <-)
(10)   ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES)))
(14)   (<- ((LIKES SALLY ?WHO)))
(17 14 10)   (<- ((LIKES ?WHO MOTIES)))
(20 17 9)   +EMPTY-CLAUSE+
--------------------------------------

Conclusion = ((<- ((LIKES SALLY SALLY))))

(13)   ((LIKES ?X ?X) <-)
(10)   ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES)))
(10)   ((LIKES SALLY ?X) <- ((LIKES ?X MOTIES)))
(14)   (<- ((LIKES SALLY ?WHO)))
(17 14 10)   (<- ((LIKES ?WHO MOTIES)))
(21 17 10)   (<- ((LIKES MOTIES MOTIES)))
(27 21 13)   +EMPTY-CLAUSE+
-----------------------------------

---

RTP Release 1.1 description.

Version 1.1: 21st March 2017

Use with test data file:  Genealogical-etc-test-data   ('load' statement at end of the file).

Version 1.01 continues to be best as a first tutorial to understand the program at code level. Plenty of comments there showing worked-execution. But the process for the user to invoke the program is clumsy.

This version has:

1. Stripped out many of the comments for improved code clarity.
2. Wrapped up execution in a new function, 'prove-it'.
3. Improved functions to print the proofs created by the program. 

All new functions at the end of the file.

Only other change is altered search strategy order in 'prove1':

.       (next-igb-list     (append new-igb-list igb-list1)) ) ; search strategy

which seems to help convergence.

---

The main test data for the new version is the genealogical axiom set which you will find in the test data mentioned above (or for an early version scroll to the bottom here).

It does lead to some tortuous proofs: for example, this one.

---

> (defvar *gg6* (mk-goal-clause '((grandfather gerry james))))

> (prove-it *gg6* *family-tree-axioms* 12)

Conclusion = ((<- ((GRANDFATHER GERRY JAMES))))

(13)   ((CHILD-OF PETER JANE JAMES) <-)
(2)   ((MALE PETER) <-)
(11)   ((CHILD-OF GERRY MARY PETER) <-)
(1)   ((MALE GERRY) <-)
(23)   ((PARENT ?X ?Z) <- ((MALE ?X) (CHILD-OF ?X ? ?Z)))
(23)   ((PARENT ?X ?Z) <- ((MALE ?X) (CHILD-OF ?X ? ?Z)))
(1)   ((MALE GERRY) <-)
(32)   ((GRANDFATHER ?X ?Z) <- ((MALE ?X) (PARENT ?X ?Y) (PARENT ?Y ?Z)))
(39)   (<- ((GRANDFATHER GERRY JAMES)))
(40 39 32)   (<- ((MALE GERRY) (PARENT GERRY ?Y1425) (PARENT ?Y1425 JAMES)))
(41 40 1)   (<- ((PARENT GERRY ?Y1425) (PARENT ?Y1425 JAMES)))
(42 41 23)   (<- ((PARENT ?Y1425 JAMES) (MALE GERRY) (CHILD-OF GERRY ?1498 ?Y1425)))
(44 42 23)   (<- ((MALE GERRY) (CHILD-OF GERRY ?1498 ?Y1425) (MALE ?Y1425) (CHILD-OF ?Y1425 ?1547 JAMES)))
(46 44 1)   (<- ((CHILD-OF GERRY ?1498 ?Y1425) (MALE ?Y1425) (CHILD-OF ?Y1425 ?1547 JAMES)))
(47 46 11)   (<- ((MALE PETER) (CHILD-OF PETER ?1547 JAMES)))
(49 47 2)   (<- ((CHILD-OF PETER ?1547 JAMES)))
(50 49 13)   +EMPTY-CLAUSE+
-------------------------------------- 

So that means it's already a superhuman reasoner, right?