0

我正在尝试了解 Z3 未解释的函数如何工作来证明这一点n=2k+1 => log(m) + k*log(m*m) == n*log(m)。为此，我使用以下内容

mylog = Function('mylog', IntSort(), IntSort())
mylog_rule1 = mylog(x*y) == mylog(x) + mylog(y)
mylog_rule2 = mylog(x**y) == y*mylog(x)
#mylog_rule3 = y*mylog(x) == mylog(x**y)  #is this rule needed ? 



rules = And(mylog_rule1, mylog_rule2, mylog_rule3)
prop = Implies(n==2*k+1, log(m) + k*log(m*m) == n*log(m))
prove(rules, prop)

我的方法一定有问题，因为这不太奏效。事实上，我什至不能prove(Implies(mylog(x*y) == mylog(x) + mylog(y), mylog(m*n) == mylog(m) + mylog(n))改变变量名。

4

1 回答 1

1

Z3 将无法有效解决此类问题。Z3 有一个非线性算术求解器 ( nlsat )。但是，此求解器不支持量词和未解释的函数。Z3 将在未来支持这一点。因此，当问题包含诸如 等未解释的函数时mylog，Z3 将使用不同的（且不完整的）求解器来进行非线性算术。该求解器将无法解决简单的非线性问题。

您的示例的另一个问题是您没有在规则中使用通用量词。prove(Implies(mylog(x*y) == mylog(x) + mylog(y), mylog(m*n) == mylog(m) + mylog(n))即使使用非线性算术的不完全求解器，也可以证明这个简单的例子。这是正确的 Z3Py 脚本（也可在此处在线获得）

mylog = Function('mylog', RealSort(), RealSort())
x, y = Reals('x y')
m, n = Reals('m n')
prove(Implies(ForAll([x,y], mylog(x*y) == mylog(x) + mylog(y)), 
      mylog(m*n) == mylog(m) + mylog(n)))
于 2013-03-01T03:45:22.750 回答