正在加载图片...
Fⅵ arayA(x)(v(x)∨(彐zy(x,y,z)→φ(x,孙,z) F VyVz((va)((r)vxp(a, y, z))-+P(c0, 9, a)), new co F Vz(Va)((a)v a(a, c1, 2))->p(c0, C1, a)), new cl F(a)(v(a)v(xp(a, c1, a))->p(c0, C1, C2), new C2 T (V(v(a)Vz(a, c1, z)) Fpc T(Vr)(v(r)vxo(a, c1, z)) T v(co)V zy(co, c1, z)) T al(co) T 3xp(co, C1, z) Figure 4: Tableau proof 4. Prove or disprove the following statements. If it is false, a counterexample should be described (9 marks) a){A→B,B→C,=C} (3 marks (b)彐x(o(x)→v(x)→(xo(x)→彐(x) (c)3.cVyVw(o(a/)Vv),3rVy(Vzv v). where o and ol are any formulas with free variables a, yand z. w is a variable not appearing in and y (3 marks Solution. (a) The tableau is show in Figure 5.(2 ks)As it is contradictory, so ac- e assertion Is d (1 mark (b) The tableau is show in Figure 6. As it is noncontradictory, so the sentence is not valid. (2 marks) Along the left path, we can construct a counterexample. Let A=co, c1,o {co},=0 (c) There are free variables. It should be transformed into its -closure form as Vz rvyVw(o(e, y, w)v v(a, y, a))-3rvy(Vap(a, y, a)Vv (a, y, a)).(1 mark) The tableau is shown in Figure 7. It is contradictory. So it is valid.(2 marks) 5. Give two sentences a= 3x(P(a)>Q)and B=(VrP(a)Q) (a) Prove that B a in semantics approach (b) Prove it by using tableau proof (2 marks (c) If a is free in Q, discuss the truth of the following assertion 3r(P(a),Q(r))H (Va P()+Q(a)). If is wrong, you should give a counterexample (3 marksF ∀x∀y∀z((∀x)(ψ(x) ∨ (∃zφ(x, y, z)) → φ(x, y, z)) F ∀y∀z((∀x)(ψ(x) ∨ (∃zφ(x, y, z)) → φ(c0, y, z)), new c0 F ∀z((∀x)(ψ(x) ∨ (∃zφ(x, c1, z)) → φ(c0, c1, z)), new c1 F (∀x)(ψ(x) ∨ (∃zφ(x, c1, z)) → φ(c0, c1, c2), new c2 T (∀x)(ψ(x) ∨ (∃zφ(x, c1, z)) F φ(c0, c1, c2) T (∀x)(ψ(x) ∨ (∃zφ(x, c1, z)) T ψ(c0) ∨ (∃zφ(c0, c1, z)) T ψ(c0) T ∃zφ(c0, c1, z) . . . Figure 4: Tableau proof 4. Prove or disprove the following statements. If it is false, a counterexample should be described: (9 marks) (a) {A → B, B → C, ¬C} |= ¬A. (3 marks) (b) ∃x(ϕ(x) → ψ(x)) → (∃xϕ(x) → ∃xψ(x)). (3 marks) (c) ∃x∀y∀w(ϕ(z/w) ∨ ψ) → ∃x∀y(∀zϕ ∨ ψ). where ϕ and ψ are any formulas with free variables x, yand z. w is a variable not appearing in ϕ and ψ. (3 marks) Solution. (a) The tableau is show in Figure 5.(2 marks) As it is contradictory, so ac￾cording to soundness theorem, the assertion is valid.(1 mark) (b) The tableau is show in Figure 6.As it is noncontradictory, so the sentence is not valid.(2 marks) Along the left path, we can construct a counterexample. Let A = {c0, c1}, ϕ = {c0}, ψ = ∅. (c) There are free variables. It should be transformed into its ∀-closure form as ∀z(∃x∀y∀w(ϕ(x, y, w)∨ ψ(x, y, z)) → ∃x∀y(∀zϕ(x, y, z)∨ψ(x, y, z))).(1 mark) The tableau is shown in Figure 7. It is contradictory. So it is valid. (2 marks) 5. Give two sentences α = ∃x(P(x) → Q) and β = (∀xP(x) → Q). (9 marks) (a) Prove that β |= α in semantics approach. (4 marks) (b) Prove it by using tableau proof. (2 marks) (c) If x is free in Q, discuss the truth of the following assertion ∃x(P(x) → Q(x)) ⊢ (∀xP(x) → Q(x)). If is wrong, you should give a counterexample. (3 marks) 4
<<向上翻页向下翻页>>
©2008-现在 cucdc.com 高等教育资讯网 版权所有