These are now here.. They are designed to be used under OCaml with the code from John Harrison's book "Practical Logic and Automated Theorem Proving" installed.

This is an embryonic system written in Prolog allowing inference rules to be implemented rather cleanly, used for proof search and the resulting proofs displayed in either linear or tree format. The author has found it useful for finding proofs in complex systems for intuitionistic logic.

The only example file given is that for **G4ip**; others will be added in due course.
Contributions and comments are welcome.

This uses an efficient method based on a *contraction-free
sequent calculus*, i.e. a calculus for which no loop-checking
is required.

- Prolog implementation (uuencoded compressed "tar" file)
- Instructions for unpacking the implementation
- Documentation of its theory
- Documentation of its implementation

- Introduction
- Implementation in Unix compressed or GZipped "tar" format
- Instructions for unpacking the implementation
- Urban's MPhil thesis documents the background theory (abstract, full thesis available from Urban.)

This uses an efficient method based on a *contraction-free
sequent calculus*, i.e. the calculus **G4ip** for which no loop-checking
is required. It is not designed to produce counter-models for
non-provable formulae. It is written in Prolog, and will be properly
documented someday. The code is designed to use very few cuts.

This uses an efficient method based on a *contraction-free
sequent calculus*, i.e. a calculus for which no loop-checking
is required. It is not designed to produce counter-models for
non-provable formulae. It is written in Prolog, and will be properly
documented someday. The code is designed to use very few cuts.
All the rules are invertible, so there is no backtracking.

12 November 2014