sequents is an implementation of Roy Dyckhoff's LJT—a sequent calculus for intuitionistic logic that is decidable and does not need loop checking

First make sure that you have smlnj installed. To build, run

./script/build.sh

Let's prove the commutativity of conjunction A ∧ B ⊃ B ∧ A. Using the ASCII approximations of the connectives, we can pipe this proposition into sequents.

➜ echo "A /\ B => B /\ A" | ./sequents

which gives the following:

Proof found!
Theorem: A ∧ B ⊃ B ∧ A.
• A, B ----> B by init
• A ∧ B ----> B by ∧L

• B, A ----> A by init
• A ∧ B ----> A by ∧L

• A ∧ B ----> B ∧ A by ∧R
• ----> A ∧ B ⊃ B ∧ A by ⊃R
QED

You can also generate LaTeX with --latex flag. Make sure that you have ebproof installed though.

➜ echo "A /\ B => B /\ A" | ./sequents --latex > out.tex
➜ pdflatex out.tex