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.

p∨¬p
Law of excluded middle
(p⇒q)⇒(¬q⇒¬p)
Contraposition
p⇒(¬p⇒q)
Contradiction
((p⇒q)⇒p)⇒p
Pierce's law
(p∨(q∧r))⇒((p∨q)∧(p∨r))
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