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

摘要

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 〈N, E, L, M〉, where N 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 N ∪ E 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 −. 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. The merge of two identical literals is represented by placing the path joining the two corresponding atom nodes 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.