Logic 1, WS 2007. Homework 5, given Nov 22, due Nov 29.

1. Prove using sequent calculus:

∀_{x}(P [x] ⇒ Q) ⊢ (∃_{x}P [x]) ⇒ Q

2. Prove using sequent calculus:

∃_{x}(P [x] ⇒ Q) ⊢ (∀_{x}P [x]) ⇒ Q

3. Prove using refutation, normal forms, and resolution that ∀_{x}(∃_{y}(S[y] ∧ V [x, y]) ⇒ (∃_{z}(C[z] ∧ V [x, z])))

is a logical consequence of

∀_{y}(S[y] ⇒ C[y]).

4. Apply the unification algorithm to: Q[x, y, z] and Q[u, h[v, v], u].