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

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Mon, 15 Aug 2016 10:29:30 -0700 (PDT)*References*: <6cd22891-fce5-42bb-9b3f-6deabee2d75e@googlegroups.com> <e80b10af-35dc-4337-84ed-186a474596ae@googlegroups.com> <4eff8892-9996-47ed-863b-3210efceb325@googlegroups.com> <96DDACD8-94BD-46BE-B90F-B33AAAA115DE@gmail.com> <c0d2f756-164e-497e-baa0-7bf29bbac42a@googlegroups.com> <965BF6AF-9241-4ACF-BE09-63C10CD8544B@gmail.com>

However, one nice aspect of propositional temporal logic (PTL) is that it is decidable. So, you could use some decision procedure for PTL such as ls4 (http://www.cs.man.ac.uk/~sudam/ , the system that we use in the TLA+ Proof System) and ask it if the formula[](P <=> Q) /\ [](R <=> S) => []( (P until R) <=> (Q until S) )

Hi Stephan,

thank you for answer. LS4 is no longer available apparently. Since you plugged it into TLAPLUS, if I enter the formula will I have the answer? Because in that case I will often use it this way.

Another question and then I dfefinitely go and buy books: why have you added the [] operators to your formula because

in the inference rule you don't need them either in the premisser or in the conclusion.

--

FL

**Follow-Ups**:**Re: [tlaplus] LTL axiomatic system***From:*Ioannis Filippidis

**Re: [tlaplus] LTL axiomatic system***From:*Stephan Merz

**References**:**LTL axiomatic system***From:*fl

**Re: LTL axiomatic system***From:*ka...@xxxxxxxxxxxxxxx

**Re: LTL axiomatic system***From:*fl

**Re: [tlaplus] LTL axiomatic system***From:*Stephan Merz

**Re: [tlaplus] LTL axiomatic system***From:*fl

**Re: [tlaplus] LTL axiomatic system***From:*Stephan Merz

- Prev by Date:
**Re: Experimenting with PlusCal / TLA+ at Dropbox** - Next by Date:
**Re: [tlaplus] LTL axiomatic system** - Previous by thread:
**Re: [tlaplus] LTL axiomatic system** - Next by thread:
**Re: [tlaplus] LTL axiomatic system** - Index(es):