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: http://logic.stanford.edu/classes/cs157/2008/cs157.html) 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!