Wednesday, December 10, 2008

Complete implementation of Chapter 9 Available


It's been a while, but finally after much grinding away, a complete implementation of all of the main First Order Logic concepts from Chapter 9 has now been added to the bleeding edge code base. In addition, for giggles :-), I've added an inference algorithm based on model elimination. You can run the FOLDemo:


to get an overview of the different capabilities. I ended up taking a class on Computational Logic (see: in order to get my head around several of the nuances involved in implementing general purpose theorem provers. Highly recommended for those so inclined. I've tried my best, 100+ test cases, to make the resolution based and model elimination implementations sound and complete, as well as reasonably efficient but no guarantees :-) Enjoy!


Ravi said...

The link to your class is very useful! One of these days, I'll work through the class notes and assignments

Alex said...

just learn java and look through the chapter 7 to 9, the implementation of FOL looks so complicated, not so much explanation there, hard to understand own my own. Is there any way to follow the code and make user understandable, which will be grate? Like this code refer to which pages or which several pages, or just add more explanation there.

ctjoreilly said...

Hey Alex,

You are correct we are lacking in the documentation department in some of the implementations. However, the main page to access the source from:

provides a high level index, which indicates which code maps to where in the book. In addition, to get more familiar with the implementations I would recommend looking at the demos:


or the JUnit test cases (see: related to the implementations:


using a debugger and stepping through the code can help a lot with clarifying how it works. I hope this helps with your explorations. If you've specific questions just let me know.