 |
 |
 |
|
 |
|
© 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).