【形式化方法】Part B: SAT And Validity（SAT和有效性）

Part B: SAT 和有效性

In Exercise 1, we've learned how to represent propositions in Z3 and how to use Z3 to obtain the solutions that make a given proposition satisfiable. In this part, we continue to discuss how to use Z3 to check the validity of propositions. Recall in exercise 2, we once used theorem prover to prove the validity of propositions, so this is another strategy.

在exercise1里咱们学会了如何在Z3中表达命题以及如何用Z3来获取可知足的解法。在这个部分，咱们继续来讨论如何用z3来检查命题的有效性。练习2中，咱们曾经用定理证实器来证实命题的有效性，因此这是另外一个策略。

Example B-1: 如前所述，命题P的有效性和可知足性之间的关系是:

valid(P) <==> unsat(~P)

咱们来看看上次的例子:

F = Or(P, Q)
    solve(Not(F))

Z3 会输出如下:

[P = False, Q = False]

~F是可知足意味着命题F是无效的。这样，如何使用Z3这样的求解器来证实一个命题的有效性就很清楚了。

Example B-2: 如今咱们来证实双重否认律(~~P - >p)是有效的:

F = Implies(Not(Not(P)), P)
    solve(Not(F))

Exercise2-1：证实排中律有效P \/ ~P

P = Bool('P') F = Or(Not(P), P) solve(Not(F))

结果输出：no solution #如下练习结果都是输出no solution

Exercise2-2：证实有效性：((P->Q)->P)->P)

P, Q = Bools('P Q') F = Implies(Implies(Implies(P, Q), P), P) solve(Not(F))

Exercise2-3：(P -> Q) -> (~Q -> ~P).

P, Q =Bools('P Q') X = Implies(P, Q) Y = Implies(Not(Q), Not(P)) F = Implies(X, Y) solve(Not(F))

Exercise2-4：(P -> Q /\ R) -> ((P -> Q) /\ (P -> R))

P, Q, R =Bools('P Q R') A = Implies(P, And(Q, R)) B = Implies(P, Q) C = Implies(P, R) F = Implies(A, And(B, C)) solve(Not(F))

# 中科大软院-形式化方法笔记-欢迎私信交流