Logic for Computer Scientists/Predicate Logic/Strategies for Resolution/SLD-Resolution

From Wikibooks, open books for an open world
< Logic for Computer Scientists‎ | Predicate Logic‎ | Strategies for Resolution
Jump to: navigation, search

SLD Resolution[edit]

In this section we will introduce a special form of linear resolution for Horn clauses. We will interpret a clause a program by notationing it in the following form:


\begin{matrix}
A &  \gets & & & \text{program clause (fact)} \\

A & \gets & B_1, \ldots, B_n && \text{ program clause }\\ 

& \gets & B_1, \ldots, B_n && \text{ goal }\\
\end{matrix}

Definition 27[edit]

Let P be a set of program clauses. Assume a selection function, which gives for a given goal \gets A_1,
\ldots, A_n one of its subgoals A_i. Further assume a goal G_i = \gets A_1, \ldots, A_m, \ldots, A_n and a selection function which selects A_m. Let C_i = A  \gets  B_1, \ldots, B_q be a variant of a clause in P, such that C_i and G_i have no variable in common. If \theta_{i+1} is most general unifier of A_m and A, the goal


G_{i+1} = \gets( A_1, \ldots, A_{m-1}, B_1, \ldots, B_q, A_{m+1}, \ldots, A_n) \theta_{i+1}

is called SLD-resolvent

Definition 28[edit]

An SLD-deduction (-refutation)of P \cup \{ G\} for a set of program clauses P and a goal clause G is a linear deduction (refutation) in which only SLD-resolution steps occur and G is the start clause.

  • An R-computed answer substitution  \theta for P \cup \{ G\} is \theta_1 \circ \ldots \circ \theta_n |_{Var(G)}, where \theta_1, \ldots,   \theta_n are the mgUs from a SLD-refutation of P \cup \{ G\} with selection function R.
  • A substitution \theta for Var(G) is an answer substitution for P   \cup \{ G\} .
  • It is a correct answer substitution for P   \cup \{   G\} , if P \models \forall G \theta

Theorem 11[edit]

Let P be a set of program clauses, G a goal clause and R a selection function. For every correct answer substitution \theta for P
\cup \{ G\} , there is an R-computed answer substitution  \sigma for P \cup \{ G\} and a substitution \gamma , such that \theta = \sigma \circ \gamma \; |_{Var(G)}

In the Section on Propositional Logic we already explained propositional tableaux and its variants, like the connection calculus and model elimination. In this section we will give model elimination in the first order case. Note that we need one more inference rule, the reduction rule, in this case

Definition 29[edit]

A clause (normalform) tableau for a set of clauses S is a tableau for S, whose nodes are literals from S and which is constructed by a (possibly infinite) sequence of applications of the following rules:

  • The tree consisting of root true and immediate successors L_1, \cdots , L_n, where C = L_1, \cdots , L_n is a new variant of a clause from S is a tableau for S (initialisation rule).
  • Let T be a tableau for S, B a branch of T, and C=L_1, \cdots ,L_n an new variant of a clause from S, such that the link-condition with mgu \sigma is satisfied. If the tree T' is constructed by extending B by the n subtrees L_i, then T'\sigma is a tableau for S (expansion rule).
  • Let T be a tableau for S, B a branch of T, L a leaf of B, and L' \in C, such that \overline{L'} and L have a mgu \sigma, than T \sigma is a tableau for S (reduction rule).

The following are three possible link conditions:

  1. No condition.
  2. Weak link condition: There is a literal L \in B and L' \in C, such that \overline{L'} and L have a mgu \sigma
  3. Strong link condition: There is a leaf L of B, and L' \in C, such that \overline{L'} and L have a mgu \sigma .

Analog to the propositional case the different link conditions result in different calculi:

  • The empty condition results in a clause normal form tableau calculus.
  • The weak condition results in a connection calculus.
  • The strong link condition results in a model elimination calculus.