Prolog and Automated Reasoning

Introduction

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., mydata.pl, 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 amazon.com.

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:

• At the bottom of this one web page introduction to Prolog are links to other intros and tutorials, some of which I've linked to below.


• Here is Barták's On-line Guide to Prolog.


• Here is an introduction to Prolog that includes an online toy implementation of Prolog that you can run via a browser.


• Here is an online HTML version of the book Adventure in Prolog. The parent company Amzi is a commercial vendor of logic-based knowledge systems based in North Carolina.


• Here's an extensive tutorial from Pomona U.


• A full PDF copy of Learn Prolog Now! by Patrick Blackburn, Johan Bos and Kristina Striegnitz can be downloaded from http://www.coli.uni-sb.de/~kris/learn-prolog-now/ or locally, at CCIS. Johan Bos has many related publications, either at: http://www.iccs.informatics.ed.ac.uk/~jbos/publications.html or his NLP work at http://www.cogsci.ed.ac.uk/~jbos/comsem/
  Here is a note to me from Bos, 3 Feb 2005, about his NLP books:

  Hi Bob,
  
  The first book is in print now at CSLI press and hopefully
  comes out very soon. (Expected beginning of 2005.) We're
  still working on V2 which we hope to finish end of this year.
  As soon as we know more about this I will let you know.
  
  Otter is the "classic" theorem prover but outperformed by
  Spass and Vampire. 
  
  Best regards,
  Johan
  
  
  

• Paul Brna has a book, Prolog Programming. A First Course. It is available in HTML or only as Postscript at http://www.scre.ac.uk/personal/pb/prologbook/book.html Here's a PDF version I've placed on my CCIS site.
• One upshot of the above that there is a paperback book now, but it doesn't appear to be a CSLI book. Instead, it's here:
• http://cs.union.edu/~striegnk/learn-prolog-now/lpnpage.php?pageid=handheld

Prolog systems to try and/or download

• SWI-Prolog has install packages for Linux, Windows, and Mac OS X. Follow the "Download" link the home page.


• JIProlog is 100% Java-based, which could be useful for any application that wished to use Java's many other facilities such as graphics and networking. It can be used free, in limited form. Otherwise, $200.


• Prolog implemented in Lisp is explained at length in Peter Norvig's book, Paradigms of Artificial Intelligence Programming: Case Studies in Common Lisp (Morgan Kaufmann, 1992). You can download all his Lisp code and run his prolog.lisp system. Note that this code has additional requires ments. Here's how it works for me on Solaris:

  USER(1): (load "auxfns")
  ; Fast loading /home/futrelle/csg120sp05/code/paip/auxfns.fasl
  T
  USER(2): (require "prolog")
  ; Loading /home/futrelle/csg120sp05/code/paip/prolog.lisp
  ;   Loading /home/futrelle/csg120sp05/code/paip/unify.lisp
  ;     Loading /home/futrelle/csg120sp05/code/paip/patmatch.lisp
  T

  His download page is at: http://www.norvig.com/paip/README.html


• Googling on:
  prolog systems download
  will lead you to others.

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.

• Otter is the best-known system. http://www-unix.mcs.anl.gov/AR/
  Some examples of setting up and running Otter can be found starting here: http://ranger.uta.edu/~cook/ai1/lectures/l6/node61.html
  then click on "Next" links to see more.
  This page has some Otter examples including an AIMA Wumpus example: http://www.cs.utsa.edu/~bylander/cs3793/


• SPASS is also widely used. http://spass.mpi-sb.mpg.de/
  Here is one-page SPASS tutorial: http://spass.mpi-sb.mpg.de/tutorial/.


• Here is a substantial list of links to automated reasoning systems/tools.

Go to Futrelle's Teaching Gateway

Return to Prof. Futrelle's home page