cvc4の実数の対数/指数

Question

対数や指数を含む実数の式のモデルを提供できるソルバーを探しています。

cvc4は、実数の対数または指数を含む関数を処理できますか？同様に、cvc4は定数eを表現できますか？

---

this questionによると、Z3は私を助けていない一定の指数を、処理することができます。

This questionは、整数の対数しか問いません。

Answer 1

私はcvc4に慣れていませんが、おそらくあなたの限界に基づいて悪用できる対数についてのいくつかの有用な特性があります。

技術的に言えば、コンピュータは（どれほど強力であっても）超越的である（有理係数を有する多項式の解法として表現することはできない）ため、eは何も知らない。

整数の対数しか取ることができないように制限されている場合は、eを派閥近似と表現してそのように解決できます。数式は単に対数を直接取るよりも少し長くなりますが、利点は、底辺が任意の有理数である対数を効果的に計算でき、整数の対数しか個別に見つけることができないことです。

eは、小数で近似できます。a/baとbの両方が整数です。

(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))はa/bがeの近似であるln(x)の近似です。明らかに、ln(x)のこの近似はln(x)の真の値に近づくので、a/bはより近似してeに近づく。私はこれを一般的な形で保ちました。a/bはeだけでなく、任意の有理数を表すことができます。

あなたの質問に完全に答えられない場合は、少なくともそれが役立つことを願っています。

---

ただ任意の例を試しました。

あなたがそれぞれ27183と10000としてaとbを考えると、私はこのクイック計算しようとした：あなたの答えのための

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

              ln(82834) = 11.32459...