Data Structure

A Binary Resolution Tree (BRT) is a data structure used for building binary resolution proofs in first order logic. Our main focus in working with BRTs is finding efficient ways of reordering resolution steps and performing surgery in order to make proofs minimal (refer to Horton & Spencer, 1998)

Consider the set of three clauses: {a, b}, {~b}, and {~a, b}. This set can be proven unsatisfiable with the (non-minimal) BRT below. All nodes are labelled by the literals which are still to be resolved (known as the clause label), while internal nodes are labelled with the letter of the atom being resolved (known as the atom label), which appears to the left of the clause label.

Minimality

A BRT can be made to look different (although it is still the same proof) if some of the resolution steps are reordered. This is done by applying AVL rotations to edges in the tree as shown in the figure below (CE is the edge being rotated). In a BRT, the edge CE can be rotated if and only if the literal in C which gets resolved at E does not come from A.

Irregularity

A BRT is said to be irregular if there exists an atom label which occcurs in a later descendent clause label. It is wasteful and unnecessary to resolve on an atom and then bring it back. Surgery can be performed on an irregular BRT, altering the proof so that the atom which causes the irregularity is not resolved the first time. Since an unnecessary resolution step has been avoided, a smaller BRT is produced.

So, a BRT is not minimal if a sequence of rotations exists which will make the BRT irregular. This is the focus of our research: to find efficient ways of determining whether a BRT can be made irregular, and if so, to efficiently perform surgery.

A rotation can be performed on the edge (e) in the above BRT, making it irregular (b is resolved upon twice on the same path).

Surgery

Preforming surgery results in the equivalent minimal BRT proof:

Minimality serves as a reduction system, eliminating some of the necessity of expensive subsumption. In theory, a O(n) where n is the number of resolutions used to generate the clause test for minimality could significantly reduce the necessity of expensive subsumptions necessary, and reduce the cost of the necessary exponential subsumptions significantly. We endeavor to provide statistical reflections of this theory applied. Currently, the MARMOSET (see Projects) is the only known attempt to implement Minimality checking and Surgery.

Since it has been shown that all clauses will be produced in minimal form during clause resolution (see Horton and Spencer, 1997 postscript gzip), the lemma exists that irregular clauses can be permanently disguarded without compromising completeness.