http://www.ksl.stanford.edu/software/IW/registry/SRC/IW-TEAM.daml Wed Feb 05 18:27:28 PST 2003 Fri May 09 17:10:50 PDT 2003 "Hyperresolution focuses on two or more clauses, requiring that one of the clauses (the nucleus) contain at least one negative literal and the remaining (the satellites) contain no negative literals. Briefly, a conclusion is yielded if a unifier (substitution of terms for variables can be found that, when applied, makes identical (except for sign) pairs of literals, one negative literal from the nucleus with one positive from a satellite. The conclusion is yielded by, ignoring the paired literals, applying the unifier simultaneously to the nucleus and the satellites and taking the union of the resulting literals. Otter's implementation of hyperresolution has two extra features. First, it can be restricted so that only ``largest'' literals in satellites can be resolved; this restriction can reduce redundancy for non-Horn clauses. Second, the negative literals in the nuclei can be evaluable instead of resolvable; This allows some amount of "programming" of Otter using built-in operations." Suppose we have as axioms the following clauses: <pre> (or (love ?x ?y) (hate ?x ?y)) (or (not (try-kill ?x ?y)) (not (love ?x ?y))) (try-kill Marcus Caesar) </pre> By substituting 'Marcus' for '?x' and 'Caesar' for '?y', we may treat the second clause as the nucleus and the first and third clauses as satellites. The opposed literals are resolved, leaving as a conclusion the resolvent <pre> (hate Marcus Caesar) </pre>