2017-11-20 3 views
0

Ich bin auf der Suche nach einem Löser, der Modelle von Formeln auf reellen Zahlen mit Logarithmen oder Exponentials bereitstellen kann.Logarithmus/Exponential von reellen Zahlen in cvc4

Kann Griff Funktionen CVC4 die Logarithmen oder Exponenten der reellen Zahlen enthalten? Ebenso kann CVC4 die Konstante e auszudrücken?


Nach this question kann z3 nur konstante Exponenten behandeln, die mir nicht helfen.

This question fragt nur über Logarithmen für ganze Zahlen.

Antwort

1

Ich bin nicht vertraut mit CVC4 aber ich vielleicht ein paar nützliche Eigenschaften über Logarithmen haben, die Sie in der Lage sein kann, auf der Grundlage Ihrer Einschränkungen zu nutzen.

Technisch gesprochen, kein Computer (egal wie mächtig) weiß, was e ist, weil es transzendent ist (kann nicht als die Lösung für eine Polynomgleichung mit rationalen Koeffizienten ausgedrückt werden).

Wenn Sie so eingeschränkt sind, dass Sie Logarithmen nur für Ganzzahlen verwenden können, können Sie e als Fraktionsapproximation angeben und so lösen. Die Formel ist etwas länger als nur den Logarithmus direkt zu nehmen, aber der Vorteil ist, dass Sie den Logarithmus, wo die Basis eine rationale Zahl ist, effektiv berechnen können, während Sie Logarithmen ganzer Zahlen nur einzeln finden.

Let e durch den Anteil a/b angenähert werden, wo sowohl a und b ganze Zahlen sind.

(a/b)^n = x 

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

Dies macht man nicht wirklich überall bekommen, so dass wir einen anderen Weg zu nehmen, die ein bisschen mehr Algebra erfordert.

(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)) 

Mit anderen Worten, ist log(base a)(x)/(1 - log(base a)(b)) eine Annäherung für ln(x) wo a/b eine Annäherung an e ist. Offensichtlich nähert sich diese Approximation für ln(x) dem realen Wert von ln(x) an, da a/b näher e ist. Hinweis ich das hier in allgemeiner Form gehalten, dass a/b jede rationale Zahl, nicht nur e darstellen könnte.

Wenn dies Ihre Frage nicht vollständig beantwortet, hoffe ich, dass es zumindest hilft.


Nur ein beliebiges Beispiel versucht.

Wenn man bedenkt, a und b als 27183 und 10000 bzw. habe ich versucht, diese schnelle Berechnung:

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

              ln(82834) = 11.32459... 
+0

Vielen Dank für Ihre Antwort! Das kann eine Abhilfe für mein Problem sein. Dennoch würde ich eine Lösung bevorzugt haben, die Annäherungen nicht erforderlich. Dies kann möglich sein, wie z.B. in 'z3' ist auch' sqrt (2) 'ausdrückbar. – Peter

+1

@Peter Wiederum ist 'e' eine transzendente Zahl. Es gibt keine Möglichkeit, es einem Computer auszudrücken, dass es genau wissen kann, was es ist.Annäherungen für "e" sind * erforderlich * im Umgang mit Computern. Irrationale Zahlen wie "sqrt (2)" können möglicherweise von einem Computer erkannt werden, da es sich, obwohl es sich nicht um eine sich wiederholende Dezimalzahl handelt, um eine Lösung für die Gleichung "x^2 - 2 = 0" handelt. – ImaginaryHuman072889

+0

Danke für die Aufklärung! Dennoch ist es im Prinzip möglich, * einige * Aufgaben zu lösen, an denen "e" beteiligt ist. Zum Beispiel ist es möglich, ein Modell für exp (2) Peter

Verwandte Themen