在线使用Z3Py证明n^5 <= 5 ^n for n >= 5 [英] Using Z3Py online to prove that n^5 <= 5 ^n for n >= 5
问题描述
使用以下代码:
n = Int('n')
s = Solver()
s.add(n >= 5)
s.add(Not( n**5 <= 5**n))
print s
print s.check()
我们得到以下输出:
[n ≥ 5, ¬(n^5 ≤ 5^n)]
unknown
也就是说Z3Py无法直接证明.
It is to say that Z3Py is not able to produce a direct proof.
现在使用代码
n = Int('n')
prove(Implies(n >= 5, n**5 <= 5**n))
Z3Py 也失败了.
一个可能的间接证明如下:
A posible indirect proof is as follows:
n = Int('n')
e, f = Ints('e f')
t = simplify(-(5 + f + 1)**5 + ((5 + f)**5 + e)*5, som=True)
prove(Implies(And(e >=0, f >= 0), t >= 0))
输出为:
proved
使用 Isabelle + Maple 的证明在:定理和算法:Isabelle 和 Maple 之间的接口中给出.克莱门斯·巴拉林.卡斯滕·霍曼.雅克·卡尔梅特.
A proof using Isabelle + Maple is given at :Theorems and Algorithms: An Interface between Isabelle and Maple. Clemens Ballarin. Karsten Homann. Jacques Calmet.
其他可能使用 Z3Py 的间接证明如下:
Other possible indirect proof using Z3Py is as follows:
n = Int('n')
e, f = Ints('e f')
t = simplify(-(5 + f + 1)**5 + ((5 + f)**5 + e)*5, som=True)
s = Solver()
s.add(e >= 0, f >= 0)
s.add(Not(t >= 0))
print s
print s.check()
输出为:
[e ≥ 0,
f ≥ 0,
¬(7849 +
9145·f +
4090·f·f +
890·f·f·f +
95·f·f·f·f +
4·f·f·f·f·f +
5·e ≥
0)]
unsat
请告诉我是否可以使用 Z3Py 进行更直接的证明.非常感谢.
Please let me know if it is possible to have a more direct proof using Z3Py. Many thanks.
推荐答案
Z3 对非线性整数算法的支持非常有限.有关详细信息，请参阅以下相关帖子:
Z3 has very limited support for nonlinear integer arithmetic. See the following related post for more information:
Z3 有一个完整的求解器(nlsat) 用于非线性实数(多项式)算术.您可以通过编写来简化您的脚本
Z3 has a complete solver (nlsat) for nonlinear real (polynomial) arithmetic. You can simplify your script by writing
n = Real('n')
e, f = Reals('e f')
prove(Implies(And(e >=0, f >= 0), -(5 + f + 1)**5 + ((5 + f)**5 + e)*5 >= 0))
Z3 在上面的问题中使用 nlsat，因为它只包含实数变量.即使问题包含整数变量，我们也可以强制 Z3 使用 nlsat.
Z3 uses nlsat in the problem above because it contains only real variables. We can also force Z3 to use nlsat even if the problem contains integer variables.
n = Int('n')
e, f = Ints('e f')
s = Tactic('qfnra-nlsat').solver()
s.add(e >= 0, f >= 0)
s.add(Not(-(5 + f + 1)**5 + ((5 + f)**5 + e)*5 >= 0))
print s
print s.check()
这篇关于在线使用Z3Py证明n^5 <= 5 ^n for n >= 5的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
