IA085: Satisfiability and Automated Reasoning
Seminar 6
Exercise 1 For each of the following first-order entailments, decide whether
it holds or not. If it does not hold, provide a counterexample. If it does, prove
it by resolution.
1. ∀x. P(x) |= ¬∃x. ¬P(x)
2. ∀x∃y. S(x, y) |= ∃y∀x. S(x, y)
3. (∀x∃y. S(x, y)) ∧ (∀x∀y. P(x) ∧ S(x, y) → P(y)) ∧ P(a) |= ∀x. P(x)
4. (∀x∀y. S(x, y)) ∧ (∀x∀y. P(x) ∧ S(x, y) → P(y)) ∧ P(a) |= ∀x. P(x)
Exercise 2 For each of the following first-order entailments with interpreted
equality, decide whether it holds or not. If it does not hold, provide a
counterexample. If it does, prove it by superposition calculus.
1. ∃x∀y. f (y) = x |= ∀x∀y. g(f (x)) = g(f (y))
2. ∀x∀y. R(x, y) → f (x) = y |= ∀x∀y∀z. R(x, y) ∧ R(x, z) → y = z
3. (∀x. f (g(x)) = x) ∧ (∀x. g(f (x)) = x) |= ∀x∃y. x = f (y)
4. ∀x∀y. (P(y) ∧ y = f (x)) → P(x) |= ∀x. P(f (f (x))) → P(x)
Exercise 3 Download the automated theorem prover Vampire and try
proving the following theorem, written in the tptp language. What does the https://tptp.org/UserDocs/
TPTPLanguage/TPTPLanguage.shtml
theorem say?
fof(ass, axiom, ! [X,Y,Z] : mult(mult(X,Y),Z) = mult(X,mult(Y,Z))).
fof(li, axiom, ! [X] : mult(e,X) = X).
fof(ri, axiom, ! [X] : mult(X,e) = X).
fof(unq, conjecture, ! [E2] : (! [X] : mult(X,E2) = X & mult(E2,X) = X) => e = E2).
Exercise 4 Use the theorem prover Vampire to prove some of the entailments
from Exercises 1 and 2.
Exercise 5 Use the theorem prover Vampire to prove the following theorem:
• Let R be a commutative ring. If R has characteristic three (i.e. 1 + 1 +
1 = 0), R includes the field F3 with three elements.