Given the following first-order formula with equality: 

(f(x) ≐ g(x) ∨ q(x)) ∧

(f(x) ≐ x) ∧

(¬(x ≐ a()) ∨ ¬q(x)) ∧

(¬p(g(f(a()))) ∧

(p(f(a())) ∨ p(x))

Prove that this formula is unsatisfiable (1) by enriching the formula with equality axioms and standard FO-resolution or (2) with the resolution calculus with paramodulation. 

Given the set of clauses 

(p(a()) ∨ p(b()) ∨ p(x) ∨ q(x) ∨ q(y) ∨ p(z) ∨ p(f(z)) ∨ ¬p(z))

Which clauses can be derived by factorization?

Given the following first-order formula with equality: 

(f(X) ≐ g(X) ∨ q(X)) ∧

(f(X) ≐ X) ∧

(¬(X ≐ a) ∨ ¬q(X)) ∧

(¬p(g(f(a))) ∧

(p(f(a)) ∨ p(X))

Prove that this formula is unsatisfiable (1) by enriching the formula with equality axioms and standard FO-resolution or (2) with the resolution calculus with paramodulation. 

Given the set of clauses 

(p(a) ∨ p(b) ∨ p(X) ∨ q(X) ∨ q(Y) ∨ p(Z) ∨ p(f(Z)) ∨ ¬p(Z))

Which clauses can be derived by factorization?

Given the first-order formula 

.

Which of the following statements hold?

Show unsatisfiability of the following formula using First-Order Resolution

Given the first-order formula p(f(x), g(b(),y)) ∨ q(b(), h(x,a(),x), b()). Which of the following elements are in the Herbrand Universe of this formula?

Transform the following formula into Skolem Normal Form: 

∃x∀y∃z. (p(x, y) ∨ ∀u∃v. q(z, u, v))

• I(a) = 0
• I(b) = 1
• I(f)(x) = 1 if x = 1, and I(f)(x) = 2 otherwise
• I(g)(x) = (x + 2) % 4
• I(p)(x) = t if x = 0, and I(p)(x) = f otherwise
• I(q)(x) = t if x >= 2, and I(q)(x) = f otherwise
• I(r)(x, y) = t if x < y, and I(r)(x, y) = f otherwise

Consider a signature with constants a, b; function symbols f, g;  predicate symbols p, q and variables x, y, z.

Given the following first-order formula Φ:

∀x∀y.(p(x,y) ∧ ¬q(f(a()), f(z), g(a(),b()))) ∧ p(z,z)

Which of the following properties hold?