README.md

LPTP - A Logic Program Theorem Prover

Note that a web-based version of LPTP is now available. Please use a modern browser such as Google Chrome.

The whole proof corpus is checked on every push under both SWI-Prolog and GNU Prolog. To run it yourself, etc/run-tests.sh swi or etc/run-tests.sh gprolog from the top directory.

How to learn LPTP?

1. Install the LPTP system (see the file INSTALL.md).

2. The directory lptp/doc contains the documentation (user.pdf).

3. In Chapter 1 you will find an example session.

   • Read Chapter 1 (Introduction). Try it out yourself.

4. Read Appendix B (Emacs mode) of the documentation.

5. Read Chapter 2 (Basic concepts of LPTP) of the documentation.

6. Read Section 3.1 (Syntax and Grammar) of Chapter 3 of the documentation.

7. Take the file lptp/lib/list/list.pr.

   • Delete all proofs.
   • Do the proofs yourself using LPTP.

8. Read the rest of the documentation.

For more information contact:

Robert F. Staerk, staerk@inf.ethz.ch