Clause trees: a tool for understanding and implementing resolution in automated reasoning

Description

A new methodology/data structure, the clause tree, is developed for automated reasoning based on resolution in first order logic. A clause tree T on a set S of clauses is a 4-tuple , where N is a set of nodes, divided into clause nodes and atom nodes, E is a set of edges, each of which joins a clause node to an atom node, L is a labeling of NuE which assigns to each clause node a clause of S, to each atom node an instance of an atom of some clause of S, and to each edge either+ or-. An instance of a clause C in S is represented by an elementary clause tree which consists of a single clause node labeled by S and joined to atom nodes labeled by the atoms of the instance. The edge joining a clause node to an atom node is labeled by the sign of the corresponding literal in the clause. A resolution is represented by unifying two atom nodes of different clause trees which represent complementary literals. In T an atom node can be adjacent either to one clause node, or to two clause nodes if it has been resolved on. The merge of two identical literals is represented by placing the path joining the two corresponding atom nodes that are leaves of the tree into the set M of chosen merge paths. The tail of the merge path becomes a closed leaf, while the head remains an open leaf which can be resolved on. The clause cl(T) that T represents, is the set of literals corresponding to the labels of the open leaves modified by the signs of the incident edges. The fundamental purpose of a clause tree T is to show that cl(T) can be derived from S using resolution. Loveland's model elimination ME, the selected literal procedure SL, and Shostak's graph construction procedure GC are explained in a unified manner using clause trees. The condition required for choosing a merge path whose head is not a leaf is given. This allows a clause tree to be built in one way (the build time) but justified as a proof in another (the proof time). The ordered clause set restriction and the foothold score restriction are explained using the operation on clause trees of merge path reversal. A new procedure called ALPOC, which combines ideas from ME, GC and OC to form a new procedure tighter than any of the top down procedures above, is developed and shown to be sound and complete. Another operation on clause trees called surgery is defined, and used to define a minimal clause tree. Any non-minimal clause tree can be reduced to a minimal clause tree using surgery, thereby showing that non-minimal clause trees are redundant. A sound procedure MinALPOC that produces only minimal clause trees is given, but whether it is complete is not known. Mergeless clause trees are shown to be equivalent to each of linear resolution, unit resolution and relative Horn sets, thereby giving short proofs of some known results. Many other new proof procedures using clause trees are discussed briefly, leaving many open questions.