Logic 1, WS 2004. Homework 5, given Nov 04, due Nov 11

1. Prove that if the formula P (a) is satisfiable, then the formula ∃_{x}P (x) is also satisfiable.

2. Prove that if the formula ∀_{x}∃_{y}P (x, y) is satisfiable, then the formula ∀_{x}P (x, f(x)) is also satisfiable.

3. Explain how to construct the Herbrand universe for the formula ∀_{x}(P (f(x), a) ⇒ Q(b, g(x))).

4. Bring into the Skolem normal form the negation of the formula:

((∀_{x}(P (x) ⇒ (Q(x) ∧ R(x)))) ∧ (∃_{x}(P (x) ∧ S(x)))) ⇒ (∃_{x}(R(x) ∧ S(x))).

5. Use the resolution method in order to infer the empty clause from the clauses of the formula obtained above.