Semantic Tableau

Enter premises and a conclusion to expand a semantic tableau automatically and test validity. Both propositional and predicate logic are supported.

Predicate-logic tableaux are generally undecidable. This tool imposes a finite expansion limit and reports an undetermined result if the procedure does not terminate within that limit.

Premises → Conclusion (Validity)

Tree structure