在线使用 Z3Py 的一些有效性证明和 Nikolaj Bjorner 提出的策略

本文介绍了在线使用 Z3Py 的一些有效性证明和 Nikolaj Bjorner 提出的策略的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！ 问题描述 引理:forall x : R, x 0 -> (x/x) = 1.Lemma: forall x : R, x <> 0 -> (x / x) = 1.证明: x = Real('x') s = Solver() s.add(Or(x >0, x < 0), Not(x/x ==1)) print s.check()输出是: unsatQed.引理:forall x y : R, x 0, y 0 -> (x/x + y/y) = 2.Lemma: forall x y : R, x <> 0, y <> 0 -> (x / x + y / y) = 2.证明:x, y = Reals('x y')s = Solver()s.add(Or(x >0, x < 0), Or(y >0, y < 0), Not(x/x + y/y ==2))print s.check()输出为:unsatQed.引理:forall x y : R, x 0, y 0 -> (x/x + x/y) = ((x + y)/y).Lemma: forall x y : R, x <> 0, y <> 0 -> (x / x + x / y) = ((x + y) / y).证明:x, y = Reals('x y')s = Solver()s.add(Or(x >0, x < 0), Or(y >0, y < 0), Not(x/x + x/y == (x+y)/y))print s.check()输出为:unsatQed.这些引理是在 http://coq.inria.fr/V8.2pl1/contribs/MapleMode.Examples.html请告诉我我使用 Z3Py 的证明是否正确，以及您是否知道使用 Z3Py 证明它们的更直接形式.非常感谢.Please let me know if my proofs with Z3Py are correct and if you know a more direct form to prove them using Z3Py. Many thanks.推荐答案使用证明"命令而不是求解器对象是一种稍微紧凑的方法.例如:There is a slightly more compact way by using the "prove" command instead of the solver object.For example:x, y = Reals('x y')prove(Implies(And(Or(x >0, x < 0), Or(y >0, y < 0)), (x/x + x/y == (x+y)/y))) 这篇关于在线使用 Z3Py 的一些有效性证明和 Nikolaj Bjorner 提出的策略的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！