Non-Macintosh software

Implementations of coherentisations of first-order logic

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.

YAPE --- Yet Another Proof Engine

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.

Counter-model generator for intuitionistic propositional logic

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

Forum and its Implementation

Decision procedure for intuitionistic propositional logic

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.

Decision procedure for propositional Dummett logic

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