UNB Synopsis Members Projects Online TP Links

© Copyrights
 
P r o j e c t s / Clause Trees

 Data Structure

The clause tree is a data structure used to build binary resolution proofs in first order logic (see Horton & Spencer, 1997 postscript gzip). Any clause can be represented by a clause tree. For example, the clause {a, b, ~c} has a corresponding clause tree:


Where o is the clause node and a, b, and c label the atom nodes. Atom nodes are joined to the clause node by edges labelled with + or -, indicating whether the corresponding literal in the clause is positive or negative.

 Resolution

If two clauses can be resolved together to give a new clause, the two corresponding clause trees can be resolved to give a new clause tree (ie. an bijective relationship exists between clauses and clause trees on resolution). Consider a second clause, {b, c, d}, corresponding to the clause tree:

Resolving the two clause trees on atom c gives the new clause tree:

 Merge Paths

Since the literal b appears twice in the tree, the two may be merged together, so b needs to be proven just once. A merge path is drawn from one b to the other as follows:

 Closed Clause Trees

An atom node leaf which is the tail of a merge path is said to be closed. An atom node leaf which is not the tail of a merge path is open. A clause tree which has no open atom leaves is a closed clause tree. A closed clause tree represents a complete proof. Consider resolving with three more clauses, {~a}, {~b}, and {~d}. This gives the following clause tree:

The clause tree is closed and therefore the proof is complete (the set of clauses is unsatisfiable).
 

Written and maintained by Brian Hunt
Last Modified: