Tableau Method: Online SAT Prover For Propositional Logic

Enter a formula to get its tableau tree. Use keyboard keys ~ & | -> <-> ( ) pqrstuvwxyz. Use keyboard CTRL + mouse wheel to increase or decrease the tableau size.

Tableau method is an algorithm that determines if a propositional formula is satisfiable. If it's not satisfiable, the negation of the formula is a tautology, according to SAT-VAL theorem. A propositional formula is satisfiable if there is at least one branch of the Tableau tree that does not get closed by the Tableau algorithm (marked green by the algorithm). If all branches are closed (marked red), the formula is not satisfiable, that is there is no assignment of boolean true/false values to the atoms of the formula that lead the formula to evaluate to true. Note that if you want to prove that a formula is valid tautology with the Tableau method, you have to build Tableau tree for negated formula. Building Tableau for formula itself does not help in determining if the formula is a tautology. The direct, non-negated formula can have some closed branches, but this does not mean the formula is not a tautology. Tautologies can also have some closed branches.

Here are some sample formulas to try. They all are not satisfiable: ¬(((p∨q)∧¬p)→q), ¬(((p→q)∧(q→r))→((p∨q)→r)), ¬(((p→q)∧(r→s))→((p∨r)→(q∨s))), ¬(¬(¬p∧¬q)→(p∨q)), ¬((p∧q)→¬(¬p∨¬q)), ¬(¬(¬p∨¬q)→(p∧q)), ¬(((p∨q)∨r)→(p∨(q∨r))).

Implemented Algorithm Description

This page uses the following procedure to draw the Tableau tree.

1. Validate formula syntax. We can operate only with well-formed formulas.
2. Convert formula to its prefix form.
3. Take the input formula as the root node. Trim double negations in front of formula. If there is still single negation left in front of the formula, mark the node as negated and remove the remaining negation from the formula beginning.
4. Next, walk the binary tree that is built on the fly, in preorder: current node, left subtree, right subtree. Start from the root node.
5. For current node, trim double negations, and if there is a negation left in the formula, remove it and mark node as negated.
6. If the current node is an atom (the node may be negated, see above), walk up the stack of preorder walk and see if there is the same atom node present in the stack, but with the opposite negate flag. If so, this branch gets closed. No need to further walk children of this node. Mark this node as closed.
7. If the current node has a prefix formula assigned to it that starts with conjunction ∧ ("and"-node), there are 2 cases: node is negated or not negated. If the node is negated, take the subformulas that are operands of conjunction, call them f₁ and f₂. Detach the old children chain of the current node, from the node, call them children. Create 2 new nodes with formulas ¬f₁ and ¬f₂, attach them as 2 new children to the current node. Attach children to the new node with formula ¬f₁, and attach deep copy of children to the new node ¬f₂. Second case: current node is not negated. Then create 2 new nodes with similar formulas f₁ and f₂, that are operands of the conjunction, but attach only node with f₁ as the only new children to the current node. Then, attach the new node f₂ as the only children to the node f₁. Then reattach the old children of current node to the node f₂. Continue the preorder walk to new children of current node.
8. If the current node has disjunction ∨ in front of its prefix formula ("or"-node), there are 2 cases as well: node is negated or not negated. Split the conjunction into its operands, formulas f₁ and f₂. If the current node is negated, note that this node's formula ¬(f₁∨f₂) is equivalent to (¬f₁∧¬f₂) according to de Morgan law. We process this as a non-negated conjunction node (see above). Similarly, the second case, if the node is not negated, we still apply de Morgan law, and process this node (f₁∨f₂) as negated conjunction node: ¬(¬f₁∧¬f₂).
9. If current node has implication → as the first operation ("follows"-node), we apply Material implication law and get (f₁→f₂) equals (¬f₁∨f₂) equals ¬(f₁∧¬f₂), so we use similar process as with conjunction.
10. A node with equivalence ↔ as the first operation is replaced by 2 implications: (f₁↔f₂) equals ((f₁→f₂)∧(f₂→f₁)).
11. Once we processed recursively all children of a node, and all branches are closed (are not satisfiable), we mark the current node as closed as well. If the node has no children and it does not have a direct contradiction with its parents, we mark this node open (satisfiable). Once we have found a satisfiable node, we can stop the whole process, the root formula is also satisfiable.