I have:
- A set of variables: the set and range they belong to (i.e. reals, integers, or a subset of these),
- A set of function definitions: compositions of common mathematical functions commonly used in computer programs (e.g. standard arithmetical operators, modulo, power and logarithm, if-then-else).
- A set of statements: equations and inequations.
I wish to use a computer program (not a service) to tell me whether each of the statements is always true, always false, or neither.
I tried to use:
Z3 Theorem Prover: it works great with linear expressions, but fails as soon as I use exponential, modulo etc.
WolframAlpha: it can handle a lot more stuff than Z3, but unfortunately it's an online service. I need a computer software that I can run offline and programmatically.
Is there any other tool I can use?
Example:
variables:
$x \in \Bbb R$
$y \in \Bbb Z \cap (0, \infty)$
function definitions:
$ floor(n) = n - ( n \mod 1 ) $
$ posInt(x) = floor( | x | ) $
statements:
$ x > 0 $
$ y < 0 $
$ |x|^x \geq 0 $
$ posInt(x) \leq x^2 $
$ (-5) ^{ 2 \cdot posInt(x) } > 0 $
$ \text{if( } y \geq 0 \text{ )then( } x^2 \geq x \text{ )else( } x^2 = x \text{ )} $
I can tell that the first statement may be true or may be false, the second one is always false, the others are always true.
Z3 can answer correctly about the first two, but not the others. WolframAlpha can handle a few more.
Is there any other program I can use? I don't need a perfect solution of course (is the problem even fully decidable?), but would like to get as many answers as possible.