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!