0

I am looking for a solver that can provide models of formulas on real numbers involving logarithms or exponentials.

Can cvc4 handle functions which contain logarithms or exponentials of real numbers? Similarly, can cvc4 express the constant e?

According to this question, z3 can only handle constant exponents, which does not help me.

This question only asks about logarithms for integers.

4

1 回答 1

1

我对 cvc4 不熟悉，但我可能有一些关于对数的有用属性，您可以根据自己的限制利用这些属性。

从技术上讲，没有计算机（无论多么强大）知道什么e是因为它是超越的（不能表示为具有有理系数的多项式方程的解）。

如果您受到限制，只能对整数取对数，则可以表示e为派系近似值并以这种方式求解。该公式最终比直接取对数要长一点，但优点是您可以有效地计算以任何有理数为底的对数，而只能单独找到整数的对数。

让用和都是整数e的分数来近似。a/bab

(a/b)^n = x

log(base a/b)(x) = n

这并不能真正带你到任何地方，所以我们必须走一条不同的路线，这需要更多的代数。

(a/b)^n = x

(a^n)/(b^n) = x

a^n = x * b^n

log(base a)(x * b^n) = n

log(base a)(x) + log(base a)(b^n) = n

log(base a)(x) + n*log(base a)(b) = n

log(base a)(x) = n - n*log(base a)(b)

log(base a)(x) = n * (1 - log(base a)(b))

n = log(base a)(x) / (1 - log(base a)(b))

换句话说，log(base a)(x) / (1 - log(base a)(b))是 的近似值，ln(x)其中a/b是 的近似值e。显然，这个近似值更接近于更接近的ln(x)实际值。请注意，我在这里以一般形式保留它，它可以表示任何有理数，而不仅仅是.ln(x)a/bea/be

如果这不能完全回答您的问题，我希望它至少有所帮助。

只是尝试了一个任意示例。

如果你分别考虑a和b作为27183和10000，我尝试了这个快速计算：

log(base 27183)(82834) / (1 - log(base 27138)(10000)) = 11.32452...

                                            ln(82834) = 11.32459...
于 2017-11-20T14:11:45.333 回答