Refinements and Additions to Resolution

The set-of-support (SOS) strategey is based on the idea that the hypotheses of a proposed theorem are generally true (in some model), hence satisfiable. Any proof will have to make use of the literals generated by the conclusion. These clauses are refered to as the set of support. Formally, a set of support $T$ is a subset of the clause set $S$ where $S \setminus T$ is satisfiable. Every resolution step must resolve upon at least one clause that is not from $S \setminus T$, i.e., one of the two clauses must either be from $T$ or a derived clause.

In positive hyperresolution, one clause, called the nucleus is resolved against a group of clauses, called the electrons, or the satellites in Otter, at each step. The nucleus must contain at least one negative literal, and electrons contain all positive literals. The result of the resolution step must contain only positive literals, i.e., all the negative literals of the nucleus must be resolved away. There is a dual strategy, called negative hyperresolution, where the nucleus must contain at least one positive literal, and the electrons contain only negative literals.

Paramodulation is a way to build the equality axioms into the inference mechanism. If $C_1$ is a clause of the form $L(t) \vee D_1$ and $C_2$ is a clause of the form $r=s \vee D_2$ where $t$ and $r$ unify with mgu $\sigma$, we can resolve by paramodulation and obtain the resulting clause $\sigma(L)(\sigma(s)) \vee \sigma(D_1) \vee \sigma(D_2)$ where $\sigma(L)(\sigma(s))$ means that one occurrence of $\sigma(t)$ is replaced by $\sigma(s)$ in $L$.