Prolog and Automated Reasoning

Professor Futrelle -- College of Computer & Information Science, Northeastern U., Boston, MA

Updated 1 January 2005 - links checked 12/13/06


This page contains useful links to online resources for Prolog and for full first-order logic theorem provers such as Otter and SPASS. Needless to say, Google works fine for virtually any kind of question you might have about the these topics.

SWI-Prolog installed on CCIS Solaris - Installs everywhere

SWI-Prolog is a large and well-developed system with a great deal of functionality. But at it's heart it is Prolog and can be used for the simplest "Hello World" examples. The SWI-Prolog home page is here. It has pointers to many other resources.
To run SWI-Prolog on the CCIS Solaris system, enter pl on the command line. To exit SWI-Prolog, enter the expression (halt). (including the final period).

The PDF and HTML versions of the SWI-Prolog manual are available on the CCIS site (these local versions are a bit out-of-date as of 12/06).

The standard way to use Prolog is to place your database of facts and rules in a file, with extension .pl, e.g.,, and then "consult" it from within Prolog. In most Prologs, including SWI, you can do this by entering [mydata]. (with the final period). The command listing. tells you what has been loaded.

"W-Prolog is an interpreter for a Prolog like language implemented in Java. The implementation is extremely portable and can be run as an applet under Java-capable web browsers." (Applet available on the W-Prolog page linked above.)

Books -- Hardcopy and on-line

Books about Prolog or mentioning Prolog number 570 on

Our Snell Library has more than 50 books with "Prolog" in the title. Search here here for "Prolog". The great majority of them have call numbers starting with QA76. The most recent edition of the Prolog text by Clocksin and Mellish is on reserve for CSU520 and CSG120 for Spring 2006.

On-line resources

There are a few sites that either offer full PDF books about Prolog online (or their .ps equivalents) or extensive tutorials that amount to the same thing:

Prolog systems to try and/or download

Full First-Order Logic theorem provers

These are full automated resolution-based First-Order Logic theorem provers. By including answer literals, they can be used for query answering.

Go to Futrelle's Teaching Gateway

Return to Prof. Futrelle's home page