SKEDSOFT

Artificial Intelligence

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

  • The OTHERS set of clauses is satisfiable. That is the case when we are given a satisfiable set of non-logical axioms and we use it as OTHERS.

Input Resolution: In Input Resolution:

  • INITIAL consists of the union of the negation of the "theorem" and of the set of non-logical axioms.
  • OTHERS usually is the set of non-logical axioms.
  • NEXT-OPEN(OPEN, C, {D1,..,Dp}) is the union of OPEN and {C}, that is, OPEN does not change in successive iterations
  • NEXT-OTHERS(OTHERS, C, {D1,..,Dp}) is the union of OTHERS, {C}, and {D1,..,Dp}.

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:

  • Q(u) OR P(A)
  • NOT Q(w) OR P(w)
  • NOT Q(x) OR NOT P(x)
  • Q(y) OR NOT P(y)

[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:

  • A Goal is the conjunction of positive literals
  • A Selection Rule is a method for selecting one of the literals of a goal (the first literal, or the last literal, etc.)
  • In SLD-Resolution, given a goal G = A1 .. An, a definite clause C: A < = B1 .. Bm, and a subgoal Ai selected from G using a Selection Rule S, where Ai and A are unifiable with MGU s, the Resolvent of G and C under S is (A1 .. Ai-1 B1 ..Bm Ai 1..An).s
  • An SLD-Derivation of a goal G given a selection rule S and a set P of definite clauses, is a sequence of triples (Gi, Ci, si), for i from 0 to k, where
  1. G0 is G
  2. for each i > 0, Ci is obtained from a clause in P by replacement of all of its variables with new variables
  3. Gi 1 is the SLD-Resolvent of Gi and Ci by use of S and with MGU si.
  • A Refutation of a goal G given definite clauses P and selection rule S, is a finite SLD-derivation of G given S and P whose last goal is the null clause. If s1 .. sk are the MGUs used in the refutation, then s = si.s2....sk is a substitution that, restricted to the variables of G, makes G true whenever the clauses of P are true.
  • The goal G succeeds for given selection rule S and set of definite clauses P if it has a refutation for P and S; otherwise it Fails.

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:

  • • WOMAN(MOTHER(v)) ; Every mother is a woman
  • • GOOD(HUSBAND(ANN)) ; The husband of Ann is good
  • • GOOD(z) < = LIKES(MOTHER(z), z); if z likes his mother then z is good

and we want to find out a woman that likes's someone's husband.

The goal can be stated as:

  • • WOMAN(x),LIKES(x,HUSBAND(y)) [NOTE: the variables x and y are implicitly existentially quantified.]

The SLD-Derivation is: