Lecture 5 Exercises

Laura Kovács

Problem 5.1

Show that positive factoring in the binary resolution system $\mathbb{BR}$ can be simulated using superposition inferences (ignoring selection functions).

🎬 Related animation: Review first-order resolution and its resolvent.

Solution

Interpret non-equality literals as equalities to a special constant $\top$. The positive factoring rule

$$\frac{p \lor p \lor C}{p \lor C}(BR)$$

can be emulated by first applying equality factoring

$$\frac{p = \top \lor p = \top \lor C}{p = \top \lor \top \neq \top \lor C}(EF)$$

and then equality resolution

$$\frac{p = \top \lor \top \neq \top \lor C}{p = \top \lor C}(ER).$$

Thus the factored clause is obtained solely via superposition rules.

Problem 5.2

Let $\succ$ be a KBO with precedence $\text{inverse} \gg \text{times}$. Compare the sides of

$$\text{inverse}(\text{times}(x,y)) = \text{times}(\text{inverse}(y), \text{inverse}(x))$$

under $\succ$ when:

1. $\text{weight}(\text{inverse}) = \text{weight}(\text{times}) = 1$
2. $\text{weight}(\text{inverse}) = 0$ and $\text{weight}(\text{times}) = 1$

Solution

1. The left-hand side has weight $2 + \text{weight}(x) + \text{weight}(y)$; the right-hand side has weight $3 + \text{weight}(y) + \text{weight}(x)$, so $\text{times}(\text{inverse}(y),\text{inverse}(x)) \succ \text{inverse}(\text{times}(x,y))$.
2. Both sides have weight $1 + \text{weight}(x) + \text{weight}(y)$. Precedence tie-breaking gives $\text{inverse} \gg \text{times}$, hence $\text{inverse}(\text{times}(x,y)) \succ \text{times}(\text{inverse}(y), \text{inverse}(x))$.

Problem 5.3

Let $\Sigma$ contain only function symbols and at least one constant. With precedence $\gg$ and weight function $w$ compatible with $\gg$, describe the ground terms of minimal weight under the induced KBO.

Solution

The minimal-weight ground terms are:

• Constants $c \in \Sigma$ of minimal weight among all constants, and
• Terms of the form $f^n(c)$ with $n > 0$, where $c$ is such a minimal-weight constant and $w(f) = 0$.

Problem 5.4

Consider the clause set

$$\begin{aligned} (1)\; & g(f(a)) = a \lor g(f(b)) = a \\ (2)\; & f(a) = a \\ (3)\; & f(b) \neq f(b) \lor f(b) = a \\ (4)\; & g(a) \neq a \end{aligned}$$

Show that $S = \{(1),(2),(3),(4)\}$ is unsatisfiable by saturating with the ground superposition calculus $\mathbb{SUP}_{\succ,\sigma}$ (including ground binary resolution) for a well-behaved $\sigma$, under:

1. $\succ$ generated by $f \gg a \gg g \gg b$ with $w(f)=0$, $w(a)=2$, $w(g)=3$, $w(b)=1$
2. $\succ$ generated by $g \gg a \gg b \gg f$ with $w(g)=0$, $w(a)=3$, $w(f)=1$, $w(b)=1$

State the selected literals and maximal terms.

Solution

Selected literals (underlined) and maximal terms (double underlined):

1. Ordering $f \gg a \gg g \gg b$:
   • $(1)\; \underline{\underline{g(f(a))} = a} \lor g(f(b)) = a$
   • $(2)\; \underline{f(a) = a}$
   • $(3)\; \underline{f(b) \neq f(b)} \lor f(b) = a$
   • $(4)\; \underline{g(a) \neq a}$
   • Equality resolution on $(3)$ gives $(5)\; \underline{f(b) = a}$.
   • Superposition of $(2)$ into $(1)$ yields $(6)\; \underline{\underline{g(a)} = a} \lor g(f(b)) = a$.
   • Resolving $(6)$ with $(4)$ produces $(7)\; \underline{g(f(b)) = a}$.
   • Superposition of $(4)$ into $(5)$ yields $(8)\; \underline{g(f(b)) \neq a}$.
   • Resolving $(7)$ and $(8)$ produces $\square$.
2. The same comparisons hold for the second ordering, so the derivation repeats and again yields $\square$.

Problem 5.5

Let $\succ$ be the KBO with precedence $f \gg a \gg b \gg c$ and weights $w(f)=w(a)=w(b)=w(c)=1$. For the clause set

$$\begin{aligned} (1)\; & a = b \lor a = c \\ (2)\; & f(a) \neq f(b) \\ (3)\; & b = c \end{aligned}$$

show that saturation under $\mathbb{SUP}_{\succ,\sigma}$ (with ground binary resolution and well-behaved $\sigma$) derives a contradiction while generating only four new clauses.

Solution

Underline selected literals and double-underline maximal terms:

1. $(1)\; \underline{\underline{a} = b} \lor a = c$
2. $(2)\; \underline{\underline{f(a)} \neq f(b)}$
3. $(3)\; \underline{\underline{b} = c}$

Steps:

1. Equality factoring on $(1)$ yields $(4)\; a = b \lor \underline{\underline{b} \neq c}$.
2. Binary resolution of $(3)$ and $(4)$ produces $(5)\; \underline{\underline{a} = b}$.
3. Superposition of $(2)$ with $(5)$ yields $(6)\; \underline{f(b) \neq f(b)}$.
4. Equality resolution on $(6)$ gives $(7)\; \square$.

Exactly four derived clauses—$(4)$ through $(7)$—are generated before the contradiction appears.