Tableau Procedure

The tableau procedure is a refutation technique which processes a formula as a tree. Each node in the tree is a set of formulas and each branch is a conjunction of its nodes. The subtrees of a node form a disjunction. A refutation is a tree where all branches contain a contradiction.

In the following we describe the tableau procedure for propositional logic.

The procedure involves systematically growing branches on the tree then checking for contradictions. Starting with a single node containing the formula to be refuted, a tree is grown in accordance with the tableau rules.

A node containing F1 ∧ F2 is grown by extending it with a subbranch containing two nodes, F1 and F2.
A node containing F1 ∨ F2 is grown by extending it with two subtrees, F1 and F2.
A node containing ¬f is grown by extending it with a subbranch of one node, t.
A node containing ¬t is grown by extending it with a subbranch of one node, f.
A node containing ¬(¬F) is grown by extending it with a subbranch of one node, F.

Other connectives, and the negation of compound formulas, can be first rewritten to an equivalent in terms of ¬, ∧, and ∨, then made subject to the rules just given. Essentially, we are rewriting to Negation Normal Form (NNF). The table below shows the rewrite rules used. Note that ⇔ is rewritten in terms of ⇒. It is intended that this is in turn rewritten to remove ⇒.

Formula	Equivalent
`F1 ⇒ F2`	`¬F1 ∨ F2`
`F1 ⇔ F2`	`(F1 ⇒ F2) ∧ (F2 ⇒ F1)`
`¬(F1 ∧ F2)`	`¬F1 ∨ ¬F2`
`¬(F1 ∨ F2)`	`¬F1 ∧ ¬F2`
`¬(F1 ⇒ F2)`	`F1 ∧ ¬F2`
`¬(F1 ⇔ F2)`	`F1 ⇔ ¬F2`

After expanding the tree we can close branches which give a contradiction. If the only connectives used are ¬, ∧, and ∨, then the only possible contradictions are branches with a node containing false, and branches with a node containing some formula F and a node containing ¬F, since F ∧ ¬F is a contradiction. If we can close all the branches in the tree, then we have a refutation.

Implementation

The following code can be found in the examples directory of the Barry's Prolog distribution.

We'll represent the tree as a list of branches, each branch being a list of the formulas at all of the nodes on the branch. We don't need to store all of the nodes separately, and the order of the formulas in the list is irrelevant as these formulas are conjuncts and conjunction is an associative and commutative operation. The procedure description given above talks of rewriting nodes, but due to the tree representation just described, we'll actually rewrite branches.

The initial tree for input formula F will be [[F]], i.e. a disjunction with a single disjunct which is the conjunction of the single conjunct F. When we create the two new subtrees with the rewrite rule for ∨, we'll replace the branch being rewritten with two branches and any formula common to both branches occurs in each branch — there is no sharing. When we expand a branch by rewriting one of its formulas, we will remove the formula from that branch. We are allowed to do this as we don't need to use that formula in a given branch more than once. Examples:

Suppose we have a tree [[a ∧ b, c]]. This tree contains one branch with two formulas: a ∧ b and c. We can rewrite this tree using the rewrite rule for ∧ into [[a, b, c]].
Suppose we have a tree [[a ∨ b, c]]. We can rewrite this tree using the rewrite rule for ∨ into [[a, c], [b, c]]. This new tree has two branches.

The following Prolog code in this section implements the procedure given earlier using the tree representation described above. First we fix a set of operators which we will need to represent the formulas of propositional logic.

:-op(200, fy, ~).                   % Negation
:-op(0, yfx, (/\)).
:-op(400, xfy, (/\)).               % Conjunction (not ISO associativity which is yfx)
:-op(0, yfx, (\/)).
:-op(500, xfy, (\/)).               % Disjunction (not ISO associativity which is yfx)
:-op(600, xfy, =>).                 % Implication
:-op(700, xfy, <=>).                % Equivalence

The procedure pl_negate(A, B) succeeds if A is the negation of B.


	pl_negate(true, false)  :- !.
pl_negate(false, true)  :- !.
pl_negate(~A, A) :- !.
pl_negate(A, ~A).

The procedure pl_tableau_transform(TreeIn, TreeOut) transforms TreeIn into TreeOut. The representation of a tree is a list of complete branches. Each branch is a conjunction of its node's formulas represented as a list of these formulas. It is here that we rewrite formulas to NNF.


	pl_tableau_transform([Branch|Branches], NewBranches) :-
	del(~ true, Branch, Rest),
	NewBranches = [[false|Rest]|Branches].
pl_tableau_transform([Branch|Branches], NewBranches) :-
	del(~ false, Branch, Rest),
	NewBranches = [[true|Rest]|Branches].
pl_tableau_transform([Branch|Branches], NewBranches) :-
	del(~(~A), Branch, Rest),
	NewBranches = [[A|Rest]|Branches].
pl_tableau_transform([Branch|Branches], [NewBranch|Branches]) :-
	del(A /\ B, Branch, Rest),
	NewBranch = [A, B|Rest].
pl_tableau_transform([Branch|Branches], NewBranches) :-
	del(A \/ B, Branch, Rest),
	NewBranches = [[A|Rest], [B|Rest]|Branches].
pl_tableau_transform([Branch|Branches], NewBranches) :-
	del(A => B, Branch, Rest),
	pl_tableau_transform([[~A \/ B|Rest]|Branches], NewBranches).
pl_tableau_transform([Branch|Branches], NewBranches) :-
	del(A <=> B, Branch, Rest),
	pl_tableau_transform([[(A => B) /\ (B => A)|Rest]|Branches], NewBranches).
pl_tableau_transform([Branch|Branches], NewBranches) :-
	del(~(A /\ B), Branch, Rest),
	pl_tableau_transform([[~A \/ ~B|Rest]|Branches], NewBranches).
pl_tableau_transform([Branch|Branches], NewBranches) :-
	del(~(A \/ B), Branch, Rest),
	pl_tableau_transform([[~A /\ ~B|Rest]|Branches], NewBranches).
pl_tableau_transform([Branch|Branches], NewBranches) :-
	del(~(A => B), Branch, Rest),
	pl_tableau_transform([[A /\ ~B|Rest]|Branches], NewBranches).
pl_tableau_transform([Branch|Branches], NewBranches) :-
	del(~(A <=> B), Branch, Rest),
	pl_tableau_transform([[A <=> ~B|Rest]|Branches], NewBranches).

The procedure pl_close_branches(TreeIn, TreeOut) creates TreeOut which is TreeIn with all closed branches removed. A closed branch is a contradiction which in our case means either false, or, F /\ ~F for any formula F. A tree where all branches have been closed will be represented by the empty list [].


	pl_close_branches([], []).
pl_close_branches([H|T], Result) :-
	member(false, H),
	!,
	pl_close_branches(T, Result).
pl_close_branches([H|T], Result) :-
	member(A, H),
	pl_negate(A, NegA),
	member(NegA, H),
	!,
	pl_close_branches(T, Result).
pl_close_branches([H|T], [H|Result]) :-
	pl_close_branches(T, Result).

The procedure pl_tableau_loop(Tree) succeeds if Tree can have all of its branches closed.


	pl_tableau_loop([]) :- !.
pl_tableau_loop(Tree0) :- 
	pl_tableau_transform(Tree0, Tree1),
	!,
	pl_close_branches(Tree1, Tree2),
	pl_tableau_loop(Tree2).
pl_tableau_loop(Tree1) :- 
	pl_close_branches(Tree1, Tree2),
	pl_tableau_loop(Tree2).

The procedure pl_tableau(Formula) succeeds if Formula can be refuted.


	pl_tableau(Formula) :-
	pl_tableau_loop([[Formula]]).

The procedure pl_tableau_tautology(Formula) succeeds if Formula is a tautology.


	pl_tableau_tautology(Formula) :-
	pl_tableau(~Formula).

References

Fitting, Melvin. First-Order Logic and Automated Theorem Proving. Springer, 1990.