Welcome to the interactive tableaux prover

This web page allows constructing proofs of propositional and first-order logic sentences using the method of semantic tableaux. To learn more about tableaux, check the Wikipedia article.

Please type in a formula to prove or choose an example from the list below.

Law of excluded middle
Pierce's law
Distributivity of ∧ over ∨
∀X (p(X)⇒q(X))⇒(∀X p(X)⇒∀X q(X))
Distributivity of ∀ over ⇒
∃X ∀Y p(X,Y)⇒∀Y ∃X p(X,Y)
Moving ∃ across ∀
∀X ∃Y p(X,Y)⇒∃Y p(a,Y)
An example of Skolemization

This theorem prover is written in Haskell; the source code package is available in the HackageDB site.

Pedro Vasconcelos <pbv@ncc.up.pt>
LIACC, University of Porto, PORTUGAL