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))
# 中科大軟院-形式化方法筆記-歡迎私信交流
轉載請註明出處，本文鏈接：https://www.uj5u.com/qita/202838.html
標籤：其他