0

I would like to delve into the capability of SMT solvers to deal with trascendental and infinitesimal elements.

Thus, I just read the paper on computing in real closed fields https://www.cl.cam.ac.uk/~gp351/infinitesimals.pdf and I would like to practise some of its examples, such as (pg 13):

msqrt2, sqrt2 = MkRoots([-2, 0, 1])
print(sqrt2)
>> root(x^2 + -2, (0, +oo), {})

However, the link to the code they offer (http://z3.codeplex.com/wikipage?title=CADE24) is not active. Also, in Z3-Py, declarations like MkRoots do not exist.

Any idea? In case this paper is out-to-date, how are trascendentals and infinitesimals treated in Z3 nowadays?

The paper also states that MetiTarski "uses the nlsat nonlinear solver in Z3", which confuses me, since I thought MetiTarski (https://www.cl.cam.ac.uk/~lp15/papers/Arith/) was a separated automatic theorem prover). Indeed, they talk about MetiTarski in related work but do not mention Z3 (also, in MetiTarski's paper https://www.cl.cam.ac.uk/~lp15/papers/Arith/MetiTarski-jar.pdf Z3 is neither mentioned).

Would you recommend any other SMT-paradigm interesting for this? Any tools to prove benchmars as the one above? Any other reading? I already know dReal, but the aforementioned paper says that "their methods are incomplete even for ∃RCF", so I would be interested in complete methods if possible.

Theo Deep
  • 666
  • 4
  • 15

1 Answers1

1

Z3's RCF related functions are in the z3.z3rcf module path, so simply import that first:

from z3       import *
from z3.z3rcf import *

msqrt2, sqrt2 = MkRoots([-2, 0, 1])
print(sqrt2)

This prints:

root(x^2 + -2, (0, +oo), {})

MetiTarski does indeed use z3: It's download page even mentions this dependency explicitly: https://www.cl.cam.ac.uk/~lp15/papers/Arith/download.html

My understanding is that reasoning with transcendentals is beyond the capability of current SMT solvers. (dReal is all about approximations, not exact solutions.) If your goal is to work on transcendentals, then your best bet is to use theorem provers. I believe there has been significant amount of work in ACL2, Coq, and Isabelle; and google results in many hits. Expecting a lot of automation would be unreasonable though, so you should be prepared to writing proofs by hand and hopefully these systems are mature enough to help you along with custom tactics and as they branch to z3 for "simpler" subgoals.

alias
  • 28,120
  • 2
  • 23
  • 40
  • Thanks for the answer, I tried using the module and it works fine :) Regarding SMTs and their ability to reason about transcendentals versus theorem provers... maybe this is mixing topics (and proving that I don't understand anything at all :p), but: don't theorem provers use SMT solvers underneath? I mean, I know they implement techniques that most solvers don't have (like induction), but is it possible to prove in a theorem provers a property on transcendentals like: `sqrt(x)^2=x`? If so, how do they do it? By calling (semi-decidable) SMT solvers like `z3.z3rcf`? – Theo Deep Jan 18 '23 at 17:53
  • 1
    A theorem prover is a general framework for proving arbitrary mathematical theorems. It doesn't suffer from "undecidability" issues, since human ingenuity can lead to proofs. (Think of Fermat's last theorem, Kepler's conjecture, or 4-color theorem. None of which can be automatically proven, but humans managed to do so, and formalized the last two and large parts of the first.) So, yes, they do use the solvers as "helpers," but they also provide the mathematical framework necessary to do "arbitrary" proofs. – alias Jan 18 '23 at 17:58
  • 1
    Example: This paper shows how to prove `e` transcendental in HOL-light: https://www.proquest.com/openview/018f4607c8fa603b8e6289715215aae0/1?pq-origsite=gscholar&cbl=4425144. I doubt there's any "fully-automatic" way of proving this in any current system. But of course, ChatGPT might prove it in a few years :-) – alias Jan 18 '23 at 17:59
  • Understood, thank you very much! I think I'm starting to see it... let's see if I get it before GPT solves all the problems :p – Theo Deep Jan 18 '23 at 18:17
  • (I'm asking this here because I think making a post about this is too "ambiguous"): in my workflow I'm using SMT solvers as a means, not as an end. If the solver says SAT, then something is done; if the solver says UNSAT, then something else is done. The point is that I wanted to test this same workflow for other kinds of formulas, e.g. sqrt(x)^2=x, formulas in RCF. But, from what we have just seen, Z3 is not very good at this. – Theo Deep Jan 18 '23 at 18:18
  • (Cont.): So one could think of replacing the SMT solver part of the workflow with theorem provers, which can prove lemmas (e.g., Fermat with degree 2) that SMT solvers (which are push-button) can't... but you'll only be proving that concrete formula! That is, in a dynamic workflow like mine (where the formulas that are queried to SMT/theorem provers solvers vary) the fact that I've proved something like Fermat for degree 2, does not imply that I have also proved Fermat for degree 3. Am I right? – Theo Deep Jan 18 '23 at 18:20
  • (Cont. end): If so, then I'm at a crossroads: (1) either I use SMT solvers which are semi-decidable (for transcendental) but allow me to automate the process or (2) I use theorem provers which allow me to do more complex tests, but take away automation. I guess it is the crossroads of life :( – Theo Deep Jan 18 '23 at 18:22
  • 1
    In a sense this is what modern provers are doing. Look at Lean/Coq/Isabelle etc. They give you the full power of a theorem prover, but automate the proofs to a large extent by using tactics (internal decision procedures), external decision procedures (like z3 or any other suitable tool); trying to give you the best of both worlds. If you're interested in any theory that doesn't have an existing decision procedure (and that's pretty much everything you seem to be interested in), then use a good theorem prover; with SMT solvers as their helpers. (Or build one yourself!) – alias Jan 18 '23 at 19:36
  • Let us [continue this discussion in chat](https://chat.stackoverflow.com/rooms/251260/discussion-between-theo-deep-and-alias). – Theo Deep Jan 19 '23 at 07:58