西安电子科技大学$2.6.2谓词逻辑推理的应用软件学院(5)A(a) ^-B(a)T (4) ES(6)A(a)T (5) I(7)-B(a)T (5) I(8)PVx(A(x) →(B(x) vC(x))(9)A(a) -→(B(a) vC(a)T (8) US(10)B(a) vC(a)T (6) (9) I(11)C(a)T (7) (10) IA(a) ^C(a)(12)T (6) (11) I(13)3x(A(x) ^C(x)T (12) EG西安电子科技大学 §2.6.2 谓词逻辑推理的应用 软件学院 (5) (6) T (4) ES T (5) I ∧ ¬ aBaA )()( aA )( (7) T (5) I ¬ aB )( (8) ∨→∀ xCxBxAx ))()(()(( P (9) ∨→ aCaBaA ))()(()( T (8) US (10) T (6) (9) I ∨ aCaB )()( (11) aC )( T (7) (10) I (12) ∧ aCaA )()( T (6) (11) I (13) ∃ ∧ xCxAx ))()(( T (12) EG