The method of Tree Proofs, also known as Semantic Tableaux, is an effective algorithm for checking the validity of formulas in various logics. The Tree Proof Generator generates tableaux for classical propositional and predicate logic.
Um...yes!
[ Tree Proof Generator ]
