Lecture 4 Lab

Laura Kovács

Problem 4.1

Apply the unification algorithm to the atoms $p(f(x,a), f(f(b,a)))$ and $p(z,f(z))$. Determine whether an mgu exists and show the intermediate steps of the algorithm.

Solution

Distinguish the unary and binary occurrences of $f$ (write them as $f_1$ and $f_2$) to avoid ambiguity:

$$E = \{\,p(f_2(x,a), f_1(f_2(b,a))) = p(z, f_1(z))\,\}.$$

The algorithm rewrites $E$ as

$$\{\,f_2(x,a) = z,\; f_1(f_2(b,a)) = f_1(z)\,\}$$

and then into

$$\{\,z = f_2(x,a),\; f_2(b,a) = z\,\}.$$

Substituting $z$ with $f_2(x,a)$ yields

$$\{\,z = f_2(x,a),\; f_2(b,a) = f_2(x,a)\,\},$$

which simplifies to

$$\{\,z = f_2(x,a),\; x = b\,\}.$$

The resulting substitution

$$\theta = \{\,z \mapsto f_2(b,a),\; x \mapsto b\,\}$$

is the most general unifier of the original atoms.

Problem 4.7

Show that the inverse of a dense order is dense. Outline a TPTP formalisation and the key steps in Vampire’s refutation (-av off).

Solution

Encode strict total order axioms and density for $r_1(x,y)$, plus clauses asserting $r_2(y,x)$ iff $r_1(x,y)$. Negate density for $r_2$ by adding a clause stating that there exist $a,b$ with no $c$ such that $r_2(a,c)$ and $r_2(c,b)$. Running Vampire (-av off) produces a refutation: the proof repeatedly superposes the inverse-direction axioms with the negated density clause until it forces a contradiction with density of $r_1$. Recording the premises, substitutions, and derived clauses from those superposition steps shows precisely how the contradiction—and therefore the density of the inverse relation—arises.

Problem 4.8

Using the group axioms (associativity, left identity, inverses), prove that the left identity element $e$ is also a right identity. Provide a TPTP encoding (axioms plus negated goal) and describe the main superposition steps in Vampire’s refutation (-av off).

Solution

Encode the axioms:

• Associativity: $! [X,Y,Z] : mult(mult(X,Y),Z) = mult(X,mult(Y,Z))$.
• Left identity: $! [X] : mult(e,X) = X$.
• Inverses: $! [X] : mult(inv(X),X) = e$.

Add the negated goal $! [X] : mult(X,e) \neq X$. Vampire refutes the set by chaining superposition steps: for example, superposing the inverse axiom with the negated goal yields clauses equating $mult(inv(X), mult(X,e))$ with $e$, which then rewrite to contradictions with the left-identity clause. Documenting the key superposition inferences (premises, mgus, conclusions) explains how the empty clause is ultimately derived, establishing that $e$ must also be a right identity.