New resource on the sidebar to your right. This should please readers wondering why vast screeds of Lisp code randomly appear here, interrupting more erudite essays on this & that.
Except as I write this, 134 of you have visited: Description: Theorem Prover in Lisp.
Here's what the READ ME at the new sidebar says.
These Common Lisp files contain AI programs which are organised around the theme of building a chatbot.
They will all run independently and were developed in LispWorks free Personal Edition.
You can use the code as you like. It's not supported and there will certainly be bugs I haven't spotted.
I think of the code as a toolkit, there to be modified.
1. Upgrades to the resolution theorem-prover improving the display of proofs + any bug fixes.
2. An AI planner, oriented both towards a toy, virtual, physical world and speech acts for conversation planning.
3. A design for 'internal emotional states' to create some 'point' for the chatbot's autonomous behaviour; we need something more interesting than a natural language interface to Wikipedia-style queries.
Plus integration of all the above.