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 は非線形演算に別の (そして不完全な) ソルバーを使用します。このソルバーは、単純な非線形問題では失敗します。

あなたの例のもう1つの問題は、ルールでユニバーサル量指定子を使用しなかったことです。単純な例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 に答える