Semantic Tableau Demo

Our team at UBC has extended the Carnap framework to support interactive proving using the semantic tableau method. By listing the initial formulas needed for a proof in a textbook page or worksheet, an instructor can insert an interactive widget for students to complete the proof.

For example, here is an exercise which shows that the set of formulas {P, P → Q, ¬P} is inconsistent.

When completed, the tree also proves that the argument P, P → Q ⊨ Q is valid.

We can also give the student an empty widget, and ask them to prove a truth-theoretic statement.

1.2 Prove that the following argument is valid:

¬A ∨ ¬B
¬B ∨ A
¬B

¬S ∧ P, ¬P ∨ R ⊨ R is valid.

The propositional logic system SL used in the UBC version of the forall x textbook is currently supported. Support for Quantified (First Order) Logic, is in the works. The next widget uses Quantified Logic.