http://www.ksl.stanford.edu/software/IW/registry/SRC/IW-TEAM.daml Fri Feb 07 11:00:57 PST 2003 Mon Mar 31 12:18:15 PST 2003 "UR-Resolution focuses on two or more clauses, requiring that one of the clauses (the nucleus) contain at least two literals and the remaining (the satellites) contain exactly one literal. Briefly, a conclusion is yielded if a unifier (substitution of terms for variables can be found that, when applied, makes identical (except for being opposite in sign) pairs of literals, one literal from the nucleus with one 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. "