Re: [tlaplus] Real numbers

[Stephan Merz <Stepha...@xxxxxxxxx>]

If there is demand, extending the SMT backend of TLAPS for handling real numbers is not difficult. What fragment of reasoning about real numbers are you interested in? Current solvers behave very erratically outside the fragment of linear real arithmetic, although several groups are looking into different approaches for effectively supporting non-linear real arithmetic: you may want to have a look at dReal (http://dreal.cs.cmu.edu/#!index.md), MetiTarski (http://www.cl.cam.ac.uk/~lp15/papers/Arith/) or Redlog (http://www.redlog.eu).

The Event-B language as defined by Abrial does not have real numbers (see e.g. http://wiki.event-b.org/images/EventB-Summary.pdf), and as far as I know there is no implementation of its provers that handles real numbers.

Stephan


On 12 Oct 2014, at 10:18, Leslie Lamport <tlapl...@xxxxxxxxx> wrote:

> I don't know what SAL is, but translating TLA+ into any backend prover is a formidable task.  You would probably wind up writing a possibly correct translation for a tiny subset of TLA+.  Since there already exists a TLA+ to Z3 translation, it would probably be easier to produce a complete translation to Z3 that can reason about reals.  I don't know if the Event-B prover handles reals.  If it does, another possible alternative is to modify their TLA+ to Event-B translator to allow you to do that.  However, that would probably be hard because I don't imagine that they translate proofs.  Hand translating to another prover seems to be the only reasonable alternative to modifying TLAPS.
> 
> Leslie