A transformation based prover for proving predicate implications
-------------------------------------------------------------------

1. You will need to download XSB from http://xsb.sourceforge.net
   XSB is a logic programming system which supports memoized or
   tabled evaluation.

2. After installing XSB, create a directory for the prover
   (henceforth assumed to be ./Prover)

3. Use the code-tar.gz and ex-tar.gz to create subdirectories
   ./Prover/Code and ./Prover/Examples in the usual way
            gunzip code-tar.gz
            tar -xvf code-tar

4. Make sure that the logic program whose predicate implications
   you want to prove is in the Examples subdirectory. Take any
   existing file in this subdirectory (e.g. mesi) to make the
   format of your program acceptable to the prover.

5. cd ./Prover/Code

6. Run XSB, and at the prompt load the "script" file
   ?- [script].

7. This will prompt you for a file name. You should enter the
   file containing the program whose predicate implication you want 
   to prove. Thus the interaction is as follows. Note that you
   should enclose the filename within quotes and end with a period.

   Enter the program file name

   'mesi'.

8. The example-file will now be dynamically loaded. You should now
   submit your proof obligation at the XSB prompt. This is as follows.
   Note that the arity of the predicates is explicitly mentioned. The
   system will now try to construct a proof and report yes/no. By
   default, the prover is in verbose mode, so it generates a description
   of the salient proof steps. You can always redirect the output.

   prove(bad_dest/2, bad_src/2).
   
9. Currently the system proves predicate implications in pure definite
   logic programs. Therefore, the above proof obligations proves that
            forall X,Y bad_dest(X, Y) => bad_src(X, Y)
   in the least Herbrand Model of the program under consideration.

10. Finally, this is a prototype system; so there (must be) plenty
    of bugs. Please send your bug reports to abhik@comp.nus.edu.sg
    with sufficient details (such as your example file). I will
    be happy to take a look whenever I get some free time.

Abhik Roychoudhury
National University of Singapore
abhik@comp.nus.edu.sg


Acknowledgements:  

A substantial part of the prover was developed in course of my 
Ph.D. work at SUNY Stony Brook.