Lecture 2 Lab

Laura Kovács

Problem 2.1

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.

Solution

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.

Problem 2.2

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.

Solution (sketch)

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.