Some Proof Strategies: From the early sixties people have looked for strategies that would simplify the search problem in theorem proving. Here are some of the strategies suggested.
1. Unit Preference: When we apply resolution if one of the premises is a unit clause (it has a single literal), the resolvent will have one less literal than the largest of the premises, thus getting closer to the desired goal {}. Thus it appears desirable to use resolution between clauses one of which is the unit clause. This unit preference is applied both when selecting from the OPEN set (i.e. at the leaves of the tree) and when we at an OR node we select an element of OTHERS to resolve with it.
2. Set of Support Strategy
When we use the Set of Support Strategy we have:
NEXT-OPEN(OPEN, C, {D1, .., Dp}) is the union of OPEN, {C}, and {D1,..,Dp}
NEXT-OTHERS(OTHERS, C, {D1,..,Dp}) is OTHERS.
In simple words, the set of support strategy uses the OPEN set as its set of support. Each application of resolution has as a premise an element of the set of support and adds that premise and the resolvent to the set of support.
Usually the INITIAL set (i.e. the initial set of support) consists of all the clauses obtained by negating the intended "theorem". The set of support strategy is complete if
Input Resolution: In Input Resolution:
In other words, in each resolution one of the premises is one of the original clauses.
In general Input Resolution is incomplete, as it can be seen with the following unsatisfiable set of clauses (from Nilsson) from which we are unable to derive FALSE using Input Resolution:
[You can use this set of clauses as both OPEN and OTHERS.]
Input resolution is complete in the case that all the clauses are Horn clauses.
Linear Resolution: Linear Resolution, also known as Ancestry-Filtered Form Strategy, is a generalization of Input Resolution. The generalization is that now in each resolution one of the clauses is one of the original clauses or it is an ancestor in the proof tree of the second premise.
Linear Resolution is complete.
SLD-Resolution: Selected Linear Resolution for Definite Clauses, or simply SLD-Resolution, is the basis for a proof procedure for theorems that are in the form of conjunctions of positive literals (this conjunction is called a Goal) given non-logical axioms that are definite clauses.
More precisely:
Theorem: SLD-Resolution is Sound and Complete for conjunctive positive goals and definite clauses.
An important consequence of this theorem is that it remains true no matter the selection rule we use to select literals in goals. Thus we can select literals as we please, for instance left-to right. An other important aspect is that the substitution s = s1.s2...sn gives us a method for finding the individuals that satisfy the goal in the structures that satisfy the clauses in P. Nothing has been said in SLD-Resolution about what rule should be used to select the clause of P to resolve with the current literal of the current goal (such a rule is called a Search rule).
Example: Suppose that we are given the following clauses:
and we want to find out a woman that likes's someone's husband.
The goal can be stated as:
The SLD-Derivation is: