latest

Author: jackeown

.gitignore

@@ -1,4 +1,5 @@
 docusaurus-site/static/vampire-runner/vampire.js
 docusaurus-site/static/vampire-runner/vampire.wasm
 docusaurus-site/node_modules
+.emcache
 vampire

docusaurus-site/docs/exercises/L2-lab.mdx

@@ -89,3 +89,35 @@ $$
 Thus exactly one inference is applicable.
 
 </details>
+
+
+## Problem 2.4
+
+Give an example of a non-tautological ground clause with at least one selected literal such that the selection is not well-behaved for any ordering.
+
+<details>
+<summary>Solution</summary>
+
+Take $p \lor \underline{p}$. The maximal literal must be $p$ under any ordering, but only one occurrence is selected, so the selection can never satisfy the “select all maximal literals” requirement.
+
+</details>
+
+
+## Problem 2.5
+
+Let
+
+$$
+S = \{\neg q \lor r,\ \neg p \lor q,\ \neg r \lor \neg q,\ \neg q \lor \neg p,\ \neg p \lor \neg r,\ \neg r \lor p,\ r \lor q \lor p\}.
+$$
+
+1. Prove $S$ is unsatisfiable using $\mathbb{BR}$.
+2. Encode $S$ in TPTP and use Vampire (run with `-av off`) to prove unsatisfiability.
+
+<details>
+<summary>Solution (sketch)</summary>
+
+1. Use binary resolution to derive unit clauses: resolve $\neg q \lor r$ with $\neg r \lor \neg q$ to obtain $\neg q$, then propagate to derive $p$ and $r$, eventually leading to a contradiction when resolving with clauses containing their negations. Any complete derivation is acceptable.
+2. Translate each clause into TPTP CNF syntax, run `vampire -av off input.tptp`, and inspect the proof output to confirm the empty clause is produced.
+
+</details>

docusaurus-site/docs/exercises/L2.mdx

@@ -112,3 +112,31 @@ where $f,g$ are function symbols, $x,y,z$ variables, and $a,b$ constants.
 Thus the inference is not simplifying under any KBO.
 
 </details>
+
+## Problem 8.5 (Hands-on Vampire)
+
+Show that the inverse of a dense order is dense. Outline a TPTP formalisation and the key steps in Vampire’s refutation (`-av off`).
+
+<details>
+<summary>Solution</summary>
+
+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.
+
+</details>
+
+## Problem 8.6 (Hands-on Vampire)
+
+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`).
+
+<details>
+<summary>Solution</summary>
+
+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.
+
+</details>