Actions

Resolution (first-order logic)

From Learning Logic for Computer Science

The resolution proof system has only one rule—the resolution proof rule—, but nevertheless it is sound and complete for refuting sets of first-order formulas in conjunctive normal form.

The proof rule is complex; a variant of the proof system—called simple resolution below—seperates two issues which are combined in the resolution rule. It has two rules, but each of them fairly simple.

Simple resolution

In the following, literals are restricted to negated and non-negated predicate formulas.

Resolution is motivated by the following lemma.

Lemma Let $K$ and $K'$ be first-order clauses and $L$ a first-order literal. Then \begin{align*} \forall \bigvee K, \forall \bigvee K' \models \forall \bigvee (K \setminus L \cup K' \setminus \bar L). \end{align*}

Proof Let $\mathcal A$ be a structure over the given signature. Assume $\mathcal A \mymodels \forall \bigvee K$ and $\mathcal A \mymodels \forall \bigvee K'$. We need to show $\mathcal A \mymodels \forall \bigvee K' '$ where $K' ' = (K \setminus L \cup K' \setminus \bar L)$. Let $x_{i_0}, \dots, x_{i_{k-1} }$ be an enumeration of $\text{vars}(K' ')$ and $a_0, \dots, a_{k-1} \in A$. By the coincidence lemma and the semantics of the universal closure (universal quantifiers), we have to show $\mathcal A, \beta \mymodels \forall \bigvee K' '$ where $\beta = \{x_{i_0} \mapsto a_0, \dots, x_{i_{k-1} } \mapsto a_{i_{k-1} }\}$. Let $x_{j_0}, \dots, x_{j_{l-1} }$ be an enumeration (possibly empty) of the variables in $\text{vars}(K \cup K') \setminus \text{vars}(K' ')$, $b_{j_0}, \dots, b_{j_{l-1} } \in A$ and set $\beta' = \{x_{j_0} \mapsto b_0, \dots, x_{j_{l-1} } \mapsto b_{j-a}\}$. Clearly, $\mathcal A, \beta \cup \beta' \not\mymodels L$ or $\mathcal A, \beta \cup \beta' \not\mymodels \bar L$, simply because of the semantics of negation. Thus, using the semantics of the disjunction, there exists $L' \in (K \setminus \{L\}) \cup (K' \setminus \{\bar L\})$ such that $\mathcal A, \beta \cup \beta' \mymodels L'$, which also means $\mathcal A, \beta \mymodels L'$, and finally $\mathcal A, \beta \mymodels (K \setminus \{L\}) \cup (K' \setminus \{\bar L\})$.


Example Let $K = \{P(f(x_0)), \neg P(b)\}$ and $K' = \{P(b)\}$. Then \begin{align*} \forall x_0 (P(f(x_0)) \vee \neg P(b)), P(b) \models \forall x_0 P(f(x_0)) \enspace. \end{align*}

This motivates the following proof rule: \begin{align} \tag{SRes} \frac{K \quad K'}{(K \setminus L) \cup (K' \setminus \bar L)} \qquad L \in K \text{ and } \bar L \in K'\enspace, \end{align} where $K$ and $K'$ are first-order clauses and $L$ is a first-order literal.

This proof rule is not complete, as the following example shows.

Example Let $K = \{P(x_0)\}$ and $K' = \{\neg P(f(x_1))\}$. The corresponding set of formulas is $\{\forall x_0 P(x_0), \forall x_1 \neg P(f(x_1))\}$, which is an unsatisfiable set of formulas. The above rule, (SRes), cannot be applied to the two clauses.

A further proof rule is needed. The one that can be used is motivated by the following example and the subsequent lemma.

Example Clearly, $\forall x_0 P(x_0)$ entails $\forall x_1 P(f(x_1))$.

Lemma Let $K$ be a first-order clause and $\sigma$ a substitution, then $\forall \bigvee K \models \forall \bigvee (K\sigma)$ for every term substitution $\sigma$.

Proof Assume $K$ is a first-order clause over some signature $\mathcal S$, say $K = \{L_0, \dots, L_{n-1}\}$ and assume $\mathcal A$ is some $\mathcal S$-structure such that $\mathcal A \mymodels \forall \bigvee K$. We need to show $\mathcal A \mymodels \forall \bigvee K\sigma$. By the semantics of $\forall$ and $\bigvee$, it is enough to show that $\mathcal A, \beta \models L_i\sigma$ for every $i<n$ and every $\mathcal A$-assignment $\beta$. From the substitution lemma, we conclude it is enough to show $\mathcal A, \beta^\sigma \models L_i$ for every $i<n$ and every $\mathcal A$-assignment $\beta$. This is true, because from the semantics of $\forall$ and $\bigvee$ and the assumption $\mathcal A \mymodels \forall\bigvee K$, we know that $\mathcal A, \beta' \mymodels L_i$ for every $i<n$ and every assignment $\beta'$.

This motivates the following proof rule: \begin{align} \tag{Sub} \frac{K}{K\sigma} \end{align}

Example A resolution proof that shows that $\forall x_0 (R(b, x_0) \leftrightarrow \neg R(x_0, x_0))$ is unsatisfiable is fairly short. First, observe that $\forall x_0 (R(b, x_0) \leftrightarrow \neg R(x_0, x_0))$ is equivalent to \begin{align*} \bigwedge \forall \bigvee \{\{R(b, x_0), R(x_0, x_0)\}, \{\neg R(b, x_0), \neg R(x_0, x_0)\}\} \enspace. \end{align*} The following is a resolution proof: \begin{array}{rll} 1 & \{R(b, x_0), R(x_0, x_0)\} & \text{premise}\\ 2 & \{R(b, b)\} & \text{(Sub) from 1 with $\{x_0 \mapsto b\}$}\\ 3 & \{\neg R(b, x_0), \neg R(x_0, x_0)\} & \text{premise}\\ 4 & \{\neg R(b, b)\} & \text{(Sub) from 3 with $\{x_0 \mapsto b\}$}\\ 5 & \{\} & \text{(SRes) from 2 and 4 with $R(b,b)$} \end{array}

The set of these two proof rules is correct and complete as far as refutation is concerned, see below.

When one wants to express that there is a proof that derives a first-order clause $K$ from a set $M$ of first-order clauses using these proof rules, one write $M \vdash_\text{sres} K$.

Resolution with a most general unifier

In the above proof system, the two proof rules are independent of each other. It is possible to combine them in one rule. This rule is, however, more complex, in particular, it involves most general unifiers:

\begin{align} \tag{Res} \frac{K \quad K'}{(K\sigma \setminus R\sigma) \cup (K'\rho\sigma \setminus R'\rho\sigma)} \qquad R \subseteq K \text{ and } R' \subseteq K' \text{ and } \rho \text{ renames } K' \text{ wrt } K \text{ and } \sigma \in \text{mgu}(R \cup \overline {R'\rho}) \end{align}

Here,

  • $\rho$ renames $K'$ wrt $K$ means that $\rho$ is an injective substitution such that $\text{vars}(K) \cap \text{vars}(K'\rho) = \emptyset$,
  • $\bar R$ for a set of clauses stands for $\{\bar L \colon L \in R\}$.

Note that the function $\text{mgu}$ (most general unifiers) is only defined for sets of positive literals. This means that all elements of $R$ must be positive literals and all elements of $R'$ must be negative literals.

Example The following shows that $\forall x_0 (R(b, x_0) \leftrightarrow \neg R(x_0, x_0))$ is unsatisfiable. \begin{array}{rll} 1 & \{R(b, x_0), R(x_0, x_0)\} & \text{premise}\\ 2 & \{\neg R(b, x_0), \neg R(x_0, x_0)\} & \text{premise}\\ 3 & \{\} & \text{(Res) from 1 and 2 with $\{R(b, x_0), R(x_0, x_0)\}$ and $\{R(b, x_0), R(x_0, x_0)\}$,} \\ & &\text{renaming $\{x_0 \mapsto x_1\}$, and mgu $\{x_0 \mapsto b, x_1 \mapsto b\}$} \end{array}

In some sense, this is a compact version of the proof in the simple resolution proof system.

When one wants to express that there is a proof that derives a first-order clause $K$ from a set $M$ of first-order clauses using the proof rule (Res), one write $M \vdash_\text{res} K$.

Correctness and completeness

The above proof systems are complete and correct.

Correctness of resolution Let $M$ be an arbitrary set of first-order clauses over some signature, $\Phi_M$ defined by $\Phi_M = \{\forall \bigvee K \colon K \in M\}$, and $K$ a first-order clause over the same signature.

  • If $M \vdash_{sres} K$, then $\Phi_M \models \forall\bigvee K$.
  • If $M \vdash_{res} K$, then $\Phi_M \models \forall\bigvee K$.

Completeness of resolution Let $M$ be an arbitrary set of first-order clauses over the same signature and $\Phi_M$ defined by $\Phi_M = \{\forall \bigvee K \colon K \in M\}$.

  • If $\Phi_M$ is unsatisfiable, then $M \vdash_{sres} \{\}$.
  • If $\Phi_M$ is unsatisfiable, then $M \vdash_{res} \{\}$.

Exercises

Exercise

  1. Zeigen Sie durch einen Resolutionsbeweis (nur Regel (Res)), dass die Formel $\bigwedge \forall \bigvee M$ mit $M$ definiert durch \[M =\{\{R(f(x_0),c),S(c,x_1)\}, \{R(x_0,c)\}, \{\neg S(c,c)\}, \{\neg R(f(x_1),x_1),S(x_1,c)\}\}\] unerfüllbar ist.
  2. Zeigen Sie durch Anwendung des Vollständigkeitssatzes für die Resolution, dass die Formel $\bigwedge \forall \bigvee M$ mit $M$ definiert durch \[M = \{\{\neg E(x_0, x_1),R(x_0,x_1)\},\{\neg R(x_0, x_1),\neg R(x_1,x_2), R(x_0,x_2)\},\{\neg R(x_0, s)\},\{\neg R(t, x_0)\}\}\] erfüllbar ist.
  3. Zeigen Sie, dass $\mu = \{x_0\mapsto f(x_4), x_1\mapsto f(x_4), x_2\mapsto f(x_4), x_3\mapsto x_4\}$ kein allgemeinster Unifikator von $\{E(x_0, x_1), E(x_2, f(x_3))\}$ ist. Nutzen Sie dazu ein geeignetes Lemma ueber Unifikatoren.


Lösung
  1. \begin{align*} 1\; & \{r(f(x_0),c),s(c,x_1)\} && \text{Voraussetzung} & \\ 2\; & \{\neg r(f(x_1),x_1),s(x_1,c)\} && \text{Voraussetzung} &\\ 3\; & \{s(c,c)\} && \text{(Res) von 1 und 2 mit $\{r(f(x_0),c)\}$ und $\{\neg r(f(x_1),x_1)$ }&\\ & &&\text{mit Umbenennung $\{x_0\mapsto x_2, x_1\mapsto x_3\}$ }&\\ & &&\text{und mgu $\{x_1\mapsto c, x_2\mapsto c, x_3\mapsto c\}$} &\\ 4\; & \{\neg s(c,c)\} && \text{Voraussetzung} &\\ 5\; & \{\} && \text{(Res) von 3 und 4 mit $\{s(c,c)\}$ und $\{\neg s(c,c)\}$ } &\\ & &&\text{ohne Umbenennung und Unifikator $\{\}$} &\\ \end{align*}
  2. Im folgenden zeigen wir, dass die Formel $\varphi = \bigwedge\forall\bigvee M$ mit \[M=\{\{\neg e(x_0, x_1),r(x_0,x_1)\},\{\neg r(x_0, x_1),\neg r(x_1,x_2),r(x_0,x_2)\},\{\neg r(x_0, s)\},\{\neg r(t, x_0)\}\}\] erfüllbar ist.

    Dazu wenden wir zunächst Resolution wie folgt auf alle möglichen Kombinationen von Klauseln an:

    \begin{align*} 1\; & \{\neg e(x_0, x_1),r(x_0,x_1)\} && \text{Voraussetzung} && \\ 2\; & \{\neg r(x_0, x_1),\neg r(x_1,x_2),r(x_0,x_2)\}, && \text{Voraussetzung}& &\\ 3\; & \{\neg r(x_0, s)\} && \text{Voraussetzung} &&\\ 4\; & \{\neg r(t, x_0)\} && \text{Voraussetzung} &&\\ 5\; & \{\neg e(x_0, x_1),\neg r(x_1,x_2),r(x_0,x_2)\} && \text{(Res) von $1$ und $2$ mit $\{r(x_0,x_1)\}$ und $\{\neg r(x_0,x_1)\}$} &\\ & && \text{ mit Umbenennung $\{x_0\mapsto x_3,x_1\mapsto x_4\}$} &\\ & && \text{ und Unifikator $\{x_{3}\mapsto x_0, x_4\mapsto x_1\}$} &\\ 6\; & \{\neg e(x_0, x_1),\neg r(x_0,x_1),r(x_0,x_2)\} && \text{(Res) von $1$ und $2$ mit $\{r(x_0,x_1)\}$ und $\{\neg r(x_1,x_2)\}$} &\\ & && \text{ mit Umbenennung $\{x_0\mapsto x_3,x_1\mapsto x_4\}$} &\\ & && \text{ und Unifikator $\{x_{3}\mapsto x_1, x_4\mapsto x_2\}$} &\\ 7\; & \{\neg e(x_0, x_0),r(x_0,x_0)\} && \text{(Res) von $2$ und $1$ mit $\{\neg r(x_0,x_1),\neg r(x_1,x_2)\}$ und $\{r(x_0,x_1)\}$} &\\ & && \text{ mit Umbenennung $\{x_0\mapsto x_3,x_1\mapsto x_4, x_2 \mapsto x_5\}$} &\\ & && \text{ und Unifikator $\{x_{1}\mapsto x_0, x_2\mapsto x_0, x_3\mapsto x_0, x_4\mapsto x_0\}$} &\\ 8\; & \{\neg e(x_0, s)\} && \text{(Res) von $1$ und $3$ mit $\{r(x_0,x_1)\}$ und $\{\neg r(x_0,s)\}$} &\\ & && \text{ mit Umbenennung $\{x_0\mapsto x_2,x_1\mapsto x_3\}$} &\\ & && \text{ und Unifikator $\{x_2\mapsto x_0, x_3\mapsto s\}$} &\\ 9\; & \{\neg e(t, x_1)\} && \text{(Res) von $1$ und $4$ mit $\{r(x_0,x_1)\}$ und $\{\neg r(t,x_0)\}$} &\\ & && \text{ mit Umbenennung $\{x_0\mapsto x_2,x_1\mapsto x_3\}$} &\\ & && \text{ und Unifikator $\{x_2\mapsto t, x_3\mapsto x_1\}$} &\\ {10}\; & \{\neg r(x_0,x_1),\neg r(x_1,s)\} && \text{(Res) von $2$ und $3$ mit $\{r(x_0,x_2)\}$ und $\{\neg r(x_0,s)\}$} &\\ & && \text{ mit Umbenennung $\{x_0\mapsto x_3,x_2\mapsto x_5\}$} &\\ & && \text{ und Unifikator $\{x_3\mapsto x_0, x_5\mapsto s\}$} &\\ {11}\; & \{\neg r(t,x_1),\neg r(x_1,x_2)\} && \text{(Res) von $2$ und $3$ mit $\{r(x_0,x_2)\}$ und $\{\neg r(t,x_0)\}$} &\\ & && \text{ mit Umbenennung $\{x_0\mapsto x_3,x_2\mapsto x_4\}$} &\\ & && \text{ und Unifikator $\{x_3\mapsto t, x_4\mapsto x_2\}$} &\\ {12}\; & \{\neg e(s,s)\} && \text{(Res) von $3$ und $7$ mit $\{\neg r(x_0,s)\}$ und $\{ r(x_0,x_0)\}$} &\\ & && \text{ mit Umbenennung $\{x_0\mapsto x_1\}$} &\\ & && \text{ und Unifikator $\{x_1\mapsto s, x_0\mapsto s\}$} &\\ {13}\; & \{\neg e(t,t)\} && \text{(Res) von $4$ und $7$ mit $\{r(t,x_0)\}$ und $\{r(x_0,x_0)\}$} &\\ & && \text{ mit Umbenennung $\{x_0\mapsto x_1\}$} &\\ & && \text{ und Unifikator $\{x_1\mapsto t, x_0\mapsto t\}$} &\\ \end{align*}

    Nun sind bis auf Umbenennung keine weitere Klausel herleitbar. Da die leere Klausel nicht enthalten ist, folgt aus der Vollständigkeit des Resolutionskalküls, dass die Formel nicht unerfüllbar sein kann. Somit ist $\varphi$ ist erfüllbar.

  3. Beachte, dass $\tau=\{x_0\mapsto x_4, x_1\mapsto f(x_5), x_2\mapsto x_4, x_0\mapsto f(x_5)\}$ ist ein Unifikator von $\{E(x_0, x_1), E(x_2, f(x_3))\}$. Wenn $\mu$ ein allgemeinster Unifikator ist, dann gibt es ein $\sigma$, sodass $\mu\sigma = \tau$. Da jedoch $\mu(x_0)=f(x_4)$ ist, müsste $f(x_4)\sigma=\tau(x_0)=x_4$ sein. Doch aufgrund der Definition von Substitution gilt $f(x_4)\sigma = f(x_4\sigma)$ und damit können wir nicht $x_4$ erhalten.

Exercise

  1. Beweisen Sie durch Überführung in konjuntive Normalform, darauf folgende Skolemisierung und einen anschließenden Resolutionsbeweis, dass die Formel $\exists x_1 L(x_1,x_1) \wedge \forall x_0\exists x_1 (\neg L(x_0,x_0) \vee (\neg P(x_1)\rightarrow P(a))) \wedge \forall x_0 \neg P(x_0)$ unerfüllbar ist.
  2. Beweisen Sie durch einen Resolutionsbeweis, dass die Formel, die das drinker paradox beschreibt, allgemeingültig ist.



Lösung
  1. Durch Umformung erhalten wir $\psi_1 = \forall x_3\forall x_1 \exists x_2\exists x_0 (L(x_0,x_0) \wedge (\neg L(x_1,x_1) \vee P(x_2) \vee P(a))\wedge\neg P(x_3))$ als äquivalente Formel in Pränexnormalform. Durch Skolemisierung erhalten wir $\psi_2 = \forall x_3\forall x_1 ( L(g(x_3,x_1,x_2),g(x_3,x_1,x_2)) \wedge (\neg L(x_1,x_1) \vee P(f(x_3,x_1)) \vee P(a))\wedge \neg P(x_3))$. Nun zeigen wir die Unerfüllbarkeit durch Resolution: \begin{align*} 1\quad & \{\neg P(x_3)\} && \text{Voraussetzung} && \\ 2\quad & \{\neg L(x_1,x_1), P(f(x_3,x_1)), P(a)\}, && \text{Voraussetzung}& &\\ 3\quad & \{\neg L(x_1,x_1), P(f(x_3,x_1))\} && \text{(Res) von $1$ und $2$ mit $\{\neg P(x_3)\}$ und $\{P(a)\}$} &\\ & && \text{ mit Umbenennung $\{x_3\mapsto x_4\}$} &\\ & && \text{ und Unifikator $\{x_{4}\mapsto a\}$} &\\ 4\quad & \{\neg L(x_1, x_1)\} && \text{(Res) von $1$ und $3$ mit $\{\neg P(x_3)\}$ und $\{P(f(x_3,x_1))\}$} &\\ & && \text{ mit Umbenennung $\{x_3\mapsto x_4\}$} &\\ & && \text{ und Unifikator $\{x_{4}\mapsto f(x_3,x_1)\}$} &\\ 5\quad & \{L(g(x_3,x_1,x_2),g(x_3,x_1,x_2))\} && \text{Voraussetzung} &\\ 6\quad & \{\} && \text{(Res) von $4$ und $5$ mit $\{\neg L(x_1, x_1)\}$ und $\{L(g(x_3,x_1,x_2),g(x_3,x_1,x_2)\}$} &\\ & && \text{ mit Umbenennung $\{x_1\mapsto x_4\}$} &\\ & && \text{ und Unifikator $\{x_4\mapsto g(x_3,x_1,x_2)\}$} &\\ \end{align*}
  2. Die Formel für das Drinker-Paradoxon lautet \[\varphi = \exists x_0\ (D(x_0) \rightarrow \forall x_1\ D(x_1)).\] Genau dann wenn $\varphi$ allgemeingültig ist, so ist $\neg \varphi$ unerfüllbar. Wir können durch Umformung die zu $\neg \varphi$ äquivalente Formel $\forall x_0\ \exists x_1( D(x_0) \wedge \neg D(x_1))$ finden. Zeigen wir nun, dass diese Formel Unerfüllbar ist, folgt direkt die Allgemeingültigkeit von $\varphi$. Dazu wandeln wir die Formel durch Skolemisierung noch zu $\psi=\forall x_0(D(x_0) \wedge \neg D(f(x_0)))$ um und wenden Resolution wie folgt an: \begin{align*} 1\quad & \{D(x_0)\} && \text{Voraussetzung} && \\ 2\quad & \{\neg D(f(x_0))\}, && \text{Voraussetzung}& &\\ 3\quad & \{\} && \text{(Res) von $1$ und $2$ mit $\{D(x_0)\}$ und $\{\neg D(f(x_0))\}$} &\\ & && \text{ mit Umbenennung $\{x_0\mapsto x_1\}$} &\\ & && \text{ und Unifikator $\{x_{0}\mapsto f(x_1)\}$} &\\ \end{align*}

Exercise

  1. Beweisen Sie durch Angabe eines Resolutionsbeweises, dass die Formel $\forall x_1\,\forall x_2\, (f(x_1)\doteq f(x_2)\rightarrow R(x_1,x_2)) \wedge \neg R(c,c)$ unerfüllbar ist. Ersetzen Sie dazu vorab das Gleichheitssymbol durch das zweistellige Relationssymbol $\text{Eq}$ und fügen Sie die Kongruenzaxiome zu den Voraussetzungen hinzu.
  2. Beweisen Sie durch Angabe eines Resolutionsbeweises, dass die Folgerung $\{a \doteq b, b\doteq c\}\models a\doteq c$ korrekt ist. Nutzen Sie dazu den Zusammenhang zwischen der Folgerungsbeziehung und der Unerfüllbarkeit, ersetzen Sie dann weiter vorab das Gleichheitssymbol durch das zweistellige Relationssymbol $\text{Eq}$ und fügen Sie die Kongruenzaxiome zu den Voraussetzungen hinzu.



Lösung
  1. Wir können zu der Formel $\varphi=\forall x_1\forall x_2 (f(x_1)\doteq f(x_2)\rightarrow R(x_1,x_2)) \wedge \neg R(c,c)$ zunächst zu der äquivalenten Formel $\varphi'=\forall x_1\forall x_2\ \left((\neg \text{Eq}(f(x_1),f(x_2))\vee R(x_1,x_2))\wedge \neg R(c,c)\right)$ umformen, sofern $\text{Eq}$ der Gleichheitsrelation entspricht. Durch hinzufügen des Kongruenzaxioms $\forall x_0\ \text{Eq}(x_0,x_0)$ können wir die Formel $\psi = \forall x_1\forall x_2\ \forall x_3\ \left((\neg \text{Eq}(f(x_1),f(x_2))\vee R(x_1,x_2))\wedge \neg R(c,c)\wedge \text{Eq}(x_3,x_3)\right)$ erhalten, die wenn $\varphi$ erfüllbar ist, auch erfüllbar ist. Durch Resolution erhalten wir die Unerfüllbarkeit von $\psi$ und damit auch von $\varphi$ wie folgt: \begin{align*} 1\; & \{\neg \text{Eq}(f(x_1),f(x_2)), R(x_1,x_2)\} && \text{Voraussetzung} & \\ 2\; & \{\neg R(c,c)\} && \text{Voraussetzung} & \\ 3\; & \{\neg \text{Eq}(f(c),f(c))\} && \text{(Res) von $1$ und $2$ mit $R=\{R(x_1,x_2)\}$ und $R'=\{\neg R(c,c)\}$} & \\ & && \text{ mit Umbenennung $\rho=\{\}$} & \\ & && \text{ und Unifikator $\{x_{1}\mapsto c, x_2\mapsto c\}$} & \\ 4\; & \{\text{Eq}(x_3,x_3)\} && \text{Voraussetzung} & \\ 5\; & \{\} && \text{(Res) von $4$ und $3$ mit $R=\{\text{Eq}(x_3,x_3)\}$ und $R'=\{\neg \text{Eq}(f(c),f(c))\}$} & \\ & && \text{ mit Umbenennung $\rho=\{\}$} & \\ & && \text{ und Unifikator $\{x_{3}\mapsto f(c)\}$} & \\ \end{align*}
  2. Die Folgerung $\{a\doteq b,b\doteq c\}\models a\doteq c$ ist genau dann korrekt, wenn $\{a\doteq b,b\doteq c,\neg a\doteq c\}$ unerfüllbar ist. Betrachten wir nun die Formel $\varphi = \forall x_0\,\forall x_1\, \forall x_2\, (\neg \text{Eq}(x_0,x_1)\vee\neg \text{Eq}(x_1,x_2)\vee \text{Eq}(x_0,x_2))$, welche äquivalent zu dem Kongruenzaxiom $\forall x_0\,\forall x_1\, \forall x_2\, (\text{Eq}(x_0,x_1)\wedge \text{Eq}(x_1,x_2))\rightarrow \text{Eq}(x_0,x_2))$ ist, so folgt, falls $\{\text{Eq}(a,b),\text{Eq}(b, c),\neg \text{Eq}(a, c), \varphi\}$ unerfüllbar ist, dass auch $\{a\doteq b,b\doteq c,\neg a\doteq c\}$ unerfüllbar sein muss. Die Unerfüllbarkeit der Formelmenge folgt nun aus folgendem Resolutionsbeweis: \begin{align*} 1\; & \{\neg \text{Eq}(x_0,x_1),\neg \text{Eq}(x_1,x_2), \text{Eq}(x_0,x_2)\} && \text{Voraussetzung} & \\ 2\; & \{\neg \text{Eq}(a,c)\} && \text{Voraussetzung} & \\ 3\; & \{\neg \text{Eq}(a,x_1),\neg \text{Eq}(x_1,c)\} && \text{(Res) von $1$ und $2$ mit $R=\{\text{Eq}(x_0,x_2)\}$ und $R'=\{\neg \text{Eq}(a, c)\}$} & \\ & && \text{ ohne Umbenennung} & \\ & && \text{ und mit Unifikator $\{x_{0}\mapsto a, x_2\mapsto c\}$} & \\ 4\; & \{\text{Eq}(a,b)\} && \text{Voraussetzung} & \\ 5\; & \{\neg\text{Eq}(b,c)\} && \text{(Res) von $4$ und $3$ mit $R=\{\text{Eq}(a,b)\}$ und $R'=\{\neg \text{Eq}(a,x_1)\}$} & \\ & && \text{ ohne Umbenennung} & \\ & && \text{ und mit Unifikator $\{x_{1}\mapsto b\}$} & \\ 6\; & \{\text{Eq}(b,c)\} && \text{Voraussetzung} & \\ 7\; & \{\} && \text{(Res) von $6$ und $5$ mit $R=\{\text{Eq}(b,c)\}$ und $R'=\{\neg \text{Eq}(b,c)\}$} & \\ & && \text{ ohne Umbenennung} & \\ & && \text{ und mit Unifikator $\{\}$} & \\ \end{align*}
Retrieved from "https://logic4free.informatik.uni-kiel.de/index.php?title=Resolution_(first-order_logic)&oldid=5053"