Ciao port of LPTP

This is an experimental port of LPTP (A Logic Program Theorem Prover, by Robert F. Staerk) focused on better integration with the Ciao assertion language and CiaoPP analysis framework.

You may consult here a copy of the original LPTP sources and documentation.

The main changes in this fork are the following:

• Packed as a Ciao bundle.
• Support for WASM-based playground (work in progress).
• Different syntax for theorems and proofs.
• Integrated into the module system.

You can check here a detailed list of changes.

Build and installation (from source)

You can fetch, build, and install this bundle using:

ciao get https://gitlab.software.imdea.org/ciao-lang/ciao_lptp

All code will be downloaded and built under the first directory specified in the CIAOPATH environment variable or ~/.ciao by default.

For developing it is recommended to define your own workspace directory and clone this repository. E.g., export CIAOPATH=~/ciao and update your PATH with eval "$(ciao-env)".

Once cloned this bundle is built with:

ciao build .

Emacs mode

Include the following into your .emacs file (change the path name):

(autoload 'lptp-mode "<<YOURPATH>>/ciao_lptp/etc/lptp-mode" 
  "Major mode for editing formal proofs" t)

(setq auto-mode-alist
  (cons '("\\.pr$" . lptp-mode) auto-mode-alist))

Playground installation

You can install in the (WebAssembly) playground with (the ciao_playground bundle is required):

ciao install --grade=wasm ciao_lptp

Then go to http://localhost:8001/playground/lptp.html

Testing your installation

Tests can be executed with:

ciao test .

This executes the original all.pl test suite (45,000 lines of formal proofs).

Additional resources

WORK IN PROGRESS

• INSTALL_LPTP.md: original installation instructions (some are not necessary in this port)

• lptp/doc: original user manual (user.pdf)

Recommended steps to work with LPTP:

1. Read Chapter 1 (Introduction), includes an example session.
2. Read Appendix B (Emacs mode)
3. Read Chapter 2 (Basic concepts of LPTP) of the documentation.
4. Read Section 3.1 (Syntax and Grammar) of Chapter 3 of the documentation.
5. Take the file lib/list/list.pl.
   • Delete all proofs.
   • Do the proofs yourself using LPTP.
6. Read the rest of the documentation.