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.

Peter
  • 401
  • 1
  • 5
  • 17

1 Answers1

1

I am unfamiliar with cvc4 but I perhaps have some useful properties about logarithms that you may be able to exploit based on your limitations.

Technically speaking, no computer (no matter how powerful) knows what e is because it is transcendental (cannot be expressed as the solution to a polynomial equation with rational coefficients).

If you are limited such that you can only take logarithms for integers, you can express e as a faction approximation and solve it that way. The formula ends up being a bit longer than just taking the logarithm directly but the advantage is that you can effectively calculate the logarithm where the base is any rational number, while only individually finding logarithms of whole numbers.

Let e be approximated by the fraction a/b where both a and b are integers.

(a/b)^n = x

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

This doesn't really get you anywhere so we have to take a different route that requires a bit more algebra.

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

In other words, log(base a)(x) / (1 - log(base a)(b)) is an approximation for ln(x) where a/b is an approximation of e. Obviously, this approximation for ln(x) gets closer to the real value of ln(x) as a/b more closely approximates e. Note I kept this in a general form here that a/b could represent any rational number, not just e.

If this doesn't answer your question fully, I hope it at least helps.

Just tried an arbitrary example.

If you consider a and b as 27183 and 10000 respectively, I tried this quick calculation:

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

                                            ln(82834) = 11.32459...
ImaginaryHuman072889
  • 4,953
  • 7
  • 19
  • 51
  • Thanks for your answer! This may be a workaround for my problem. Still, I would have preferred a solution that does not require approximations. This may be possible, as e.g. in `z3`, also `sqrt(2)` is expressible. – Peter Nov 24 '17 at 08:51
  • 1
    @Peter Again, `e` is a transcendental number. There is no way to express it to a computer that it can know precisely what it is. Approximations for `e` are *required* when dealing with computers. Irrational numbers such as `sqrt(2)` can possibly be known by a computer because, although it is not a repeating decimal, it is a solution to the equation `x^2 - 2 = 0`. – ImaginaryHuman072889 Nov 25 '17 at 02:01
  • Thanks for the clarification! Still, it is in principle possible to solve *some* tasks involving `e`. For example, it is possible to find a model for `exp(2) – Peter Nov 26 '17 at 15:24
  • @Peter No problem. If that is the case, can you (at least, temporarily, until/if someone else answers) mark my answer as the accepted answer? – ImaginaryHuman072889 Nov 27 '17 at 11:57