Home

Propositional Intuitionistic Logic G4IP

This is a sequent-style prover for propositional intuitionistic logic using a contraction-free calculus
which requires no loop-check.

Roy Dyckhoff
Contraction-Free Sequent Calculi for Intuitionistic Logic.
J. Symb. Log. 57(3): 795-807 (1992)

Results
Query

formula :=
ATOM | Verum | Falsum
| formula & formula
| formula v formula
| formula -> formula
| formula <-> formula
| ! formula (* intuitionistic negation with ! A translated into A -> Falsum *)
| # formula (* this is used only internally and is not an external connective for users *)

Input is an end-sequent of the form:
Set of formulae => Set of formulae
so if you want to test if a formula A is a theorem of Int then you have to type in
=> A
otherwise you will get an internal error.

Info