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))

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