【形式化方法】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))

# 中科大軟院-形式化方法筆記-歡迎私信交流