[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Stephan Merz <Stepha...@xxxxxxxxx>*Date*: Sun, 12 Oct 2014 11:23:29 +0200*References*: <7c4fd2f4-f223-4642-8ace-d0eb49b378d7@googlegroups.com> <6a2d4bd2-e02f-4292-b7c6-02fe09624f8d@googlegroups.com>

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

**Follow-Ups**:**Re: [tlaplus] Real numbers***From:*John Baugh

**Re: [tlaplus] Real numbers***From:*Michael Leuschel

**References**:**Real numbers***From:*John Baugh

**Re: Real numbers***From:*Leslie Lamport

- Prev by Date:
**Re: Real numbers** - Next by Date:
**Re: [tlaplus] Real numbers** - Previous by thread:
**Re: Real numbers** - Next by thread:
**Re: [tlaplus] Real numbers** - Index(es):