LEAP

Logic Engine for Argument by Pointing

Enter a formula to prove:

Syntax: -> implication, & and, | or, ~ not, forall x. / exists x., T true, F false

Example theorems:

Current Goal

Open Goals

Proof Tree

QED

Proof complete!