Non-Macintosh software

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.

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

Forum and 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.)

Decision procedure 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. 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.

• Here it is!

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.

• Here it is!