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

Selective Linear Definite (SLD) Resolution

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

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

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

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

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.