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

Question

引理：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()

输出是：

  unsat

Qed。

引理：forall xy : 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()

输出是：

unsat

Qed。

引理：forall xy : 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()

输出是：

unsat

Qed。

这些引理是使用 Coq + Maple 在

请让我知道我的 Z3Py 证明是否正确，以及您是否知道使用 Z3Py 证明它们的更直接形式。非常感谢。

score 3 · Accepted Answer

通过使用“证明”命令而不是求解器对象，有一种更紧凑的方法。例如：

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

1 回答 1