PLAISTED'S THEOREM PROVER
                      Written by David A. Plaisted
                      Contributed by Norbert Fuchs,
            Department of Computer Science, Zurich University
                   Shelved on the 3rd of October 1988


This is  a C Prolog  program: a theorem  prover based on  the simplified
problem reduction format. It comes as three files:

    PLAISTED.PRE        This file.
    PLAISTED.PL         The source.
    TESTS.PL            Instructions and examples.

To find out how to run it, read the comments at the head of each file.               



CHECKED ON EDINBURGH-COMPATIBLE (POPLOG) PROLOG :
    No.


PORTABILITY :
    Contains a number of C-Prolog idiosyncrasies.


INTERNAL DOCUMENTATION :
    A description of how to run the program, plus a number of examples.