# Logic for Computer Scientists/Predicate Logic/Resolution

## ResolutionEdit

In the propositional case we defined the resolution inference rule by "cutting away" a pair of complementary literals in two clauses which are resolved upon. In the first order case however this is not always sufficient:

${\displaystyle {\begin{matrix}C_{1}:&p(x)\lor q(x)\\C_{2}:&\lnot p(f(x))\end{matrix}}}$

In these two clauses there are no complementary literals, however, after substituting the term ${\displaystyle f(a)}$  for the variable ${\displaystyle x}$  in ${\displaystyle C_{1}}$  and ${\displaystyle a}$  for ${\displaystyle x}$  in ${\displaystyle C_{2}}$  we arrive at:

${\displaystyle {\begin{matrix}C_{1}':&p(f(a))\lor q(f(a))\\C_{2}':&\lnot p(f(a))\end{matrix}}}$

Now we can apply the inference rule from propositional logic and arrive at the resolvent ${\displaystyle q(f(a))}$ .

Another possibility is to substitute ${\displaystyle f(x')}$  for ${\displaystyle x}$  in ${\displaystyle C_{1}}$  to get

${\displaystyle C_{1}'':p(f(x'))\lor q(f(x'))}$

and then we can have the resolvent ${\displaystyle q(f(x'))}$  from ${\displaystyle C_{1}''}$  and ${\displaystyle C_{2}}$ , which is in a certain sense more general then the resolvent derived previously.

## Definition 18Edit

A substitution ${\displaystyle \sigma }$  is a function, which maps variables to terms and which is the identical mapping almost everywhere. Hence it can be represented as

${\displaystyle \sigma =\{x_{1}/t_{1},\cdots ,x_{n}/t_{n}\}}$

If ${\displaystyle t_{1},\cdots ,t_{n}}$  are groundterms, we call ${\displaystyle \sigma }$  a ground substitution. The empty substitution is notated by ${\displaystyle \epsilon }$  .

## Definition 19Edit

Let ${\displaystyle \theta =\{x_{1}/t_{1},\cdots ,x_{n}/t_{n}\}}$  be a substitution and ${\displaystyle E}$  an expression (i.e. a literal or a term), then ${\displaystyle E\theta }$  is the expression, obtained from ${\displaystyle E}$  by replacing simultaneously each occurrence of ${\displaystyle X_{i},1\leq i\leq n}$  in ${\displaystyle E}$  by the term ${\displaystyle t_{i}}$ .

Example:
With ${\displaystyle \theta =\{x/a,y/f(b),z/e\}}$  and ${\displaystyle E=p(x,y,z)}$ , we get ${\displaystyle E\theta =p(a,f(b),c)}$

## Definition 20Edit

Let ${\displaystyle \sigma =\{x_{1}/t_{1},\cdots ,x_{n}/t_{n}\}}$  and ${\displaystyle \lambda =\{y_{1}/s_{1},\cdots ,y_{m}/s_{m}\}}$  be substitutions. Then the composition of substitutions, denoted by ${\displaystyle \sigma \circ \lambda }$ , is the substitution, which is obtained from ${\displaystyle \{x_{1}/t_{1}\lambda ,\cdots ,x_{n}/t_{n}\lambda ,y_{1}/s_{1},\cdots ,y_{m}/s_{m}\}}$  by deleting any element ${\displaystyle x_{j}/t_{j}\lambda }$  for which ${\displaystyle t_{j}\lambda =x_{j}}$  and any element ${\displaystyle y_{i}/s_{i}}$  such that ${\displaystyle y_{i}\in \{x_{1},\cdots ,x_{n}\}}$  .
Example:

## Definition 21Edit

Let ${\displaystyle \{E_{1},\cdots ,E_{n}\}}$  be a set of expressions and ${\displaystyle \theta }$  a substitution, ${\displaystyle \theta }$  is unifier for ${\displaystyle \{E_{1},\cdots ,E_{n}\}}$  iff

${\displaystyle E_{1}\theta =E_{2}\theta =\cdots E_{n}\theta }$

.

A unifier ${\displaystyle \theta }$  is called most general unifier iff for every unifier ${\displaystyle \sigma }$  there is a substitution ${\displaystyle \lambda }$  such that ${\displaystyle \sigma =\theta \circ \lambda }$ .

In the following we discuss an algorithm for computing most general unifiers. For this we assume a set of terms ${\displaystyle \{t_{1},\cdots ,t_{n}\}}$  to be unified. First we transform this into a set of equations by introducing a new variable not yet occurring in this set, say ${\displaystyle y}$  and by defining the set of equations

${\displaystyle N=\{y=t_{1},\cdots ,y=t_{n}\}}$

We will now transform this set such that its unifiers stay invariant, where a ${\displaystyle \sigma }$  is a unifier of a set of ${\displaystyle \{s_{1}=t_{1},\cdots ,s_{n}=t_{n}\}}$  if ${\displaystyle \{s_{1}\sigma =t_{1}\sigma ,\cdots ,s_{n}\sigma =t_{n}\sigma \}}$  holds.

 Unification Given a set of expression. Transform it into a set of equations ${\displaystyle N}$  as defined above. Apply the following transformation rules as long as possible: ${\displaystyle {\frac {R\uplus \{t=x\}}{R\uplus \{x=t\}}}}$  Orient where ${\displaystyle x}$  is a variable and ${\displaystyle t}$  a non-variable term ${\displaystyle {\frac {R\uplus \{s=s\}}{R}}}$  Delete ${\displaystyle {\frac {R\uplus \{f(s_{1},\dots ,s_{n})=f(t_{1},\dots ,t_{n})\}}{R\uplus \{s_{1}=t_{1},\dots ,s_{n}=t_{n}\}}}}$  Decompose (Termreduction) ${\displaystyle {\frac {R\uplus \{x=t\}}{R[x/t]\uplus \{x=t\}}}}$  Eliminate (Elimination of variable I) if ${\displaystyle x}$  not in ${\displaystyle t}$ , but in ${\displaystyle R}$  ${\displaystyle {\frac {R\uplus \{x=y\}}{R[x/y]\uplus \{x=y\}}}}$ Coalesce (Elimination of variable II) if ${\displaystyle x\neq y}$  in ${\displaystyle R}$  ${\displaystyle {\frac {R\uplus \{f(s_{1},\dots ,s_{m})=g(t_{1},\dots ,t_{n})\}}{\mbox{FAIL}}}}$  Conflict if ${\displaystyle f\neq g}$  or ${\displaystyle m\neq n}$  ${\displaystyle {\frac {R\uplus \{x=t\}}{\mbox{FAIL}}}}$  Occur Check if ${\displaystyle x}$  in ${\displaystyle t}$

## Theorem 7Edit

Let ${\displaystyle N}$  be a set of expressions. The above unification algorithm terminates. If it returns ${\displaystyle FAIL}$ , there is no unifier for ${\displaystyle N}$ , otherwise ${\displaystyle N}$  is transformed into a set of equation ${\displaystyle \{y_{1}=u_{1},\cdots ,y_{m}=u_{m}\}}$ , which represents the most general unifier for ${\displaystyle N}$ .

## Definition 22Edit

Let two or more literals of a clause ${\displaystyle C}$  have a unifier ${\displaystyle \sigma }$ , then ${\displaystyle C\sigma }$  is called a factor of ${\displaystyle C}$ .

Example:
With ${\displaystyle C=\{p(x),p(f(y)),\lnot q(x)\}}$  and ${\displaystyle \sigma =\{x/f(y)\}}$  we get the factor ${\displaystyle C\sigma =\{p(f(y)),\lnot q(f(y))\}}$

## Definition 23Edit

Let ${\displaystyle C_{1}}$  and ${\displaystyle C_{2}}$  be two clauses with no variables in common, such that ${\displaystyle L_{1}\in C_{1}}$  and ${\displaystyle L_{2}\in C_{2}}$  and ${\displaystyle L_{1}}$  and ${\displaystyle L_{2}}$  have a most general unifier ${\displaystyle \sigma }$ . A binary resolvent of ${\displaystyle C_{1}}$  and ${\displaystyle C_{2}}$  is

${\displaystyle (C_{1}\sigma -L_{1}\sigma )\cup (C_{2}\sigma -L_{2}\sigma )}$

Example: Given ${\displaystyle C_{1}=\{p(x),q(x)\}}$  and ${\displaystyle C_{2}=\{\lnot p(a),r(x)\}}$ . After renaming ${\displaystyle C_{2}}$  into ${\displaystyle C_{2}=\{\lnot p(a),r(y)\}}$  we get the resolvent ${\displaystyle \{q(a),r(y)\}}$  by using the most general unifier ${\displaystyle \{x/a\}}$ .

We often depict resolvent graphically, e.g.

## Definition 24Edit

A resolvent of two clauses ${\displaystyle C_{1}}$  and ${\displaystyle C_{2}}$  is one of the following binary resolvents:

• a binary resolvent of ${\displaystyle C_{1}}$  and ${\displaystyle C_{2}}$
• a binary resolvent of ${\displaystyle C_{1}}$  and a factor of ${\displaystyle C_{2}}$
• a binary resolvent of a factor of ${\displaystyle C_{1}}$  and ${\displaystyle C_{2}}$
• a binary resolvent of a factor of ${\displaystyle C_{1}}$  and a factor of ${\displaystyle C_{2}}$

Example:

Given ${\displaystyle C_{1}=\{p(x),p(f(y)),r(g(y))\}}$  and ${\displaystyle C_{2}=\{\lnot p(f(g(a))),q(b)\}}$ .

A factor of ${\displaystyle C_{1}}$  is ${\displaystyle C_{1}\prime =\{p(f(y)),r(g(y))\}}$ . A binary resolvent of ${\displaystyle C_{1}\prime }$  and ${\displaystyle C_{2}}$  and hence also of ${\displaystyle C_{1}}$  and ${\displaystyle C_{2}}$  is ${\displaystyle C_{3}=\{r(g(g(a))),q(b)\}}$ .

The following lemma is used in the completeness proof of resolution.

## Lemma 5 (Lifting lemma)Edit

If ${\displaystyle C_{1}\prime }$  and ${\displaystyle C_{2}\prime }$  are instances of ${\displaystyle C_{1}}$  and ${\displaystyle C_{2}}$ , respectively, and ${\displaystyle C\prime }$  is a resolvent of ${\displaystyle C_{1}\prime }$  and ${\displaystyle C_{2}\prime }$ , then there is a resolvent ${\displaystyle C}$  of ${\displaystyle C_{1}}$  and ${\displaystyle C_{2}}$  such that ${\displaystyle C\prime }$  is an instance of ${\displaystyle C}$ .

Figure 1

## Theorem 8Edit

A set ${\displaystyle S}$  of clauses is unsatisfiable iff the empty clause can be derived from ${\displaystyle S}$  by resolution.
Proof:
Assume that ${\displaystyle S}$  is unsatisfiable. Let ${\displaystyle A=\{A_{1},A_{2},\ldots \}}$  be the ground atom set of ${\displaystyle S}$ , hence the Herbrand basis. Let ${\displaystyle T}$  be a complete binary tree, as given in Figure 2. According to Herbrand's theorem (version1) there exists a closed finite semantic tree ${\displaystyle T'}$ . There are two cases:

• If ${\displaystyle T'}$  consists only of one node (hence the root), The interpretation to be collected from the empty branch in this tree falsifies only the empty clause. Hence the empty clause must be in ${\displaystyle S}$ .
• Assume ${\displaystyle T'}$  consists of more than one node. Then there must be an inference node ${\displaystyle N}$  in ${\displaystyle T'}$ , hence both its descendants ${\displaystyle N_{1}}$  and ${\displaystyle N_{2}}$  are failure nodes. If such a node would not exist, every node would have at least one non-failure node, which would mean that there is at least an infinite path in ${\displaystyle T'}$ , which would violate, that fact that it is a finite closed semantic tree. Let ${\displaystyle N,N_{1},N_{2}}$  given as described above; and let
${\displaystyle {\begin{matrix}I(N)&=&\{m_{1},m_{2},\ldots ,m_{n}\}I(N_{1})&=&\{m_{1},m_{2},\ldots ,m_{n},m_{n},m_{n+1}\}I(N_{2})&=&\{m_{1},m_{2},\ldots ,m_{n},m_{n},\lnot m_{n+1}\}\end{matrix}}}$

Now, let ${\displaystyle C_{1}'}$  and ${\displaystyle C_{2}'}$  be ground instances of clauses ${\displaystyle C_{1}}$  and ${\displaystyle C_{2}}$ , such that ${\displaystyle C_{1}'}$  is falsified by ${\displaystyle I(N_{1})}$  and ${\displaystyle C_{2}'}$  by ${\displaystyle I(N_{2})}$ , such that both are not falsified by ${\displaystyle I(N)}$ .

Hence we have ${\displaystyle \lnot m_{n+1}\in C_{1}'}$  and ${\displaystyle m_{n+1}\in C_{2}'}$  and we can construct the resolvent

${\displaystyle C'=(C_{1}'-\{\lnot m_{n+1}\})\cup (C_{2}'-\{m_{n+1}\})}$

${\displaystyle C'}$  must be false in ${\displaystyle I(N)}$ , because both ${\displaystyle (C_{1}'-\lnot m_{n+1})}$  and ${\displaystyle (C_{2}'-m_{n+1})}$  are false in ${\displaystyle I(N)}$ . According to the Lifting Lemma 5 there exists a resolvent ${\displaystyle C}$  of ${\displaystyle C_{1}}$  and ${\displaystyle C_{2}}$ , such that ${\displaystyle C'}$  is a ground instance of ${\displaystyle C}$ . Let ${\displaystyle T\;''}$  be the closed semantic tree for ${\displaystyle S\cup \{C\}}$  , obtained from ${\displaystyle T'}$  by deleting all nodes below the first node which falsifies ${\displaystyle C'}$ . Note, that ${\displaystyle S}$  is unsatisfiable if and only if ${\displaystyle S\cup \{C\}}$  is unsatisfiable. Clearly, ${\displaystyle T\;''}$  has less nodes than ${\displaystyle T'}$  and we now can iterate this process until only the root of the semantic tree is remaining. This, however is only possible if the empty clause ${\displaystyle \square }$  is derivable. For the opposite direction, assume that ${\displaystyle \square }$  is derivable by resolution from ${\displaystyle S}$  and let ${\displaystyle R_{1},\ldots ,R_{k}}$  the resolvents constructed during this process. Assume ${\displaystyle S}$  is satisfiable and ${\displaystyle M}$  to be a model for ${\displaystyle S}$ . From the correctness lemma according to the propositional case we known, that if a model satisfies two clauses it also satisfies its resolvent. Therefore ${\displaystyle M}$  has to satisfy ${\displaystyle R1,\ldots ,R_{k}}$ ; this, however, is impossible, because one of this resolvents is ${\displaystyle \square }$ .

Figure 2

## ProblemsEdit

#### Problem 14 (Predicate)Edit

Indicate in each case a derivation of the empty clause with predicate-logical resolution!

1. ${\displaystyle \{\{p(x,0,x)\},\{p(x,s(y),s(z)),\lnot p(x,y,z)\},\{\lnot p(s(s(s(0))),s(s(0)),u)\}\}}$
2. ${\displaystyle \{\{q(x),q(s(x))\},\{\lnot q(x),\lnot q(s(s(x)))\}\}}$
(${\displaystyle \star }$ )
3. ${\displaystyle \{\{\lnot r(x,f(x),y),\lnot r(x,g(y),z)\},\{r(c,u,i(v)),r(h(u),v,j(v))\}\}}$

${\displaystyle \Box }$

#### Problem 15 (Predicate)Edit

Show the following Lifting lemma by means of induction over the term- and formula construction: Is ${\displaystyle F}$  a predicate-logical formula, and ${\displaystyle {\mathcal {I}}}$  a fitting interpretation for

${\displaystyle F}$  and ${\displaystyle F[x/t]}$ . Then

${\displaystyle {\mathcal {I}}(F[x/t])={\mathcal {I}}_{[x/{\mathcal {I}}(t)]}(F),}$

is valid, if ${\displaystyle t}$  does not contain any variable that ${\displaystyle [x/t]}$  is laced

by the substitution in ${\displaystyle F}$ .
${\displaystyle \Box }$

#### Problem 16 (Predicate)Edit

Compute - if possible - the most general unifier of following sets of clauses:

1. ${\displaystyle \{p(x,a),p(f(c),y)\}}$
2. ${\displaystyle \{p(f(x),a,x),p(y,z,z)\}}$
3. ${\displaystyle \{q(x,x),q(g(y),y)\}}$
4. ${\displaystyle \{r(x,x),r(a,h(y))\}}$

${\displaystyle \Box }$

#### Problem 17 (Predicate)Edit

Determine all direct resolvents of the following pairs of clauses:

1. ${\displaystyle \{\lnot p(x),q(x,b)\}}$  and ${\displaystyle \{p(a),q(a,b)\}}$
2. ${\displaystyle \{p(x),p(f(x))\}}$  and ${\displaystyle \{\lnot p(x),\lnot p(f(f(x)))\}}$
3. ${\displaystyle \{\lnot q(c,g(c))\}}$  and ${\displaystyle \{\lnot p(x),q(x,x)\}}$
4. ${\displaystyle \{\lnot p(x,y,z),\lnot p(y,u,v),\lnot p(x,v,w),p(z,u,w)\}}$  and ${\displaystyle \{p(g(x,y),x,y)\}}$

${\displaystyle \Box }$

#### Problem 18 (Predicate)Edit

Compute - if possible - the most general unifier of following sets of clauses:

1. ${\displaystyle \{o(x,x),o(a,f(y))\}}$
2. ${\displaystyle \{p(x,a),p(f(c),y)\}}$
3. ${\displaystyle \{q(g(x),a,x),q(y,z,z)\}}$
4. ${\displaystyle \{r(x,x),r(h(y),y)\}}$

${\displaystyle \Box }$

#### Problem 19 (Predicate)Edit

Determine all direct resolvents of the following pairs of clauses:

1. ${\displaystyle \{\lnot p(x),\lnot p(b),q(x,b)\}}$  and ${\displaystyle \{p(a),q(a,b)\}}$
2. ${\displaystyle \{r(x),r(f(x))\}}$  and ${\displaystyle \{\lnot r(x),\lnot r(f(f(x)))\}}$
3. ${\displaystyle \{\lnot s(c,g(c))\}}$  and ${\displaystyle \{s(x,x),\lnot t(x)\}}$

${\displaystyle \Box }$

#### Problem 20 (Predicate)Edit

Give for the following set of clauses (a) a linear derivation, (b) a derivation with unit resolution, (c) a further (maximally short) derivation of the empty clause by means of predicate-logical resolution!

${\displaystyle \{\{\lnot e(x),o(s(x))\},\{\lnot e(x),\lnot o(s(x)),e(s(s(x)))\},\{e(a)\},\{\lnot o(s(s(s(s(s(a))))))\}\}}$

${\displaystyle \Box }$

#### Problem 21 (Predicate)Edit

Indicate in each case a derivation of the empty clause with predicate-logical resolution!

1. ${\displaystyle \{\{p(x,0,x)\},\{p(x,s(y),s(z)),\lnot p(x,y,z)\},\{\lnot p(s(s(s(0))),s(s(0)),u)\}\}}$
2. ${\displaystyle \{\{q(x),q(s(x))\},\{\lnot q(x),\lnot q(s(s(x)))\}\}}$
(${\displaystyle \star }$ )
3. ${\displaystyle \{\{\lnot r(x,f(x),y),\lnot r(x,g(y),z)\},\{r(c,u,i(v)),r(h(u),v,j(v))\}\}}$

${\displaystyle \Box }$