西安电子科技大学$2.6.2谓词逻辑推理的应用软件学院-P→(x)-A(x), (V x)A(x)-Q = Q-→P(1)-P→(日x)-A(x)P(2)T (1) E-P-→-(x)A(x)(3)(Vx)A(x)→PT (2) EP(4)(Vx)A(x)-Q(5)((Vx)A(x)→Q) ^(Q-→(Vx)A(x)T (4) E(6)Q→(Vx)A(x)T (5) IQ→P(7)T (3) (6) I西安电子科技大学 §2.6.2 谓词逻辑推理的应用 软件学院 (1) (2) P T (1) E (3) T (2) E (4) P (5) T (4) E (6) T (5) I (7) T (3) (6) I ¬P → ( ∃x)¬A(x) ¬P →¬( ∀x)A(x) ( ∀x)A(x) →P ( ∀x)A(x) ↔Q (( ∀x)A(x) →Q) ∧(Q → ( ∀x)A(x)) Q → ( ∀x)A(x)) Q →P ¬P → ( ∃x)¬A(x), ( ∀x)A(x) ↔Q ⇒ Q → P