Fr(P(x)→Q) Q F P(c), new constant c F彐x(P(x)→Q) F彐r(P(x)→Q) F P(t)>Q, for a ground term t P(c) T P(t) T P(c) F Q F Q Figure 8: Tableau proof of 5.(b) Fvr(vrP(x)→Q(x)) F Vc P(a)Q(co), new constant co T Va P(az) Q(co) T丑x(P(x)→Q(x) T P(c1))Q(c1), new constant cI F P(c1) T Q(c1) VaP(r) Var P() T P(c1) T P(co) F proof of 5.(c)F ∃x(P(x) → Q) T ∀xP(x) → Q F ∀xP(x) T Q F P(c), new constant c F ∃x(P(x) → Q) F P(c) → Q T P(c) F Q ⊗ F ∃x(P(x) → Q) F P(t) → Q, for a ground term t T P(t) F Q ⊗ Figure 8: Tableau proof of 5.(b) F ∀x(∀xP(x) → Q(x)) F ∀xP(x) → Q(c0), new constant c0 T ∀xP(x) F Q(c0) T ∃x(P(x) → Q(x)) T P(c1) → Q(c1), new constant c1 F P(c1) T Q(c1) T ∀xP(x) T P(c1) ⊗ T ∀xP(x) T P(c0) . . . Figure 9: Tableau proof of 5.(c) 9