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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Tue, 16 Aug 2016 08:58:42 +0200*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> <dd1defda-329c-49bd-875c-f994e119779b@googlegroups.com>

Indeed, but there are similar decision procedures, e.g. TRP++ (https://cgi.csc.liv.ac.uk/~konev/software/trp++/) or the Logics Workbench (http://www.lwb.unibe.ch, you can even enter your formula via a Web form).
LEMMA ASSUME NEW TEMPORAL P, NEW TEMPORAL Q PROVE [](P <=> Q) => ([]<>P <=> []<>Q) BY PTL
(P <=> Q) => ([]<>P <=> []<>Q) is not valid since P and Q are assumed to be equivalent only in the initial state, and nothing is known about their relationship in other states. More generally, a rule (temporal sequent) Gamma, F |- B for some set of formulas Gamma is equivalent to the sequent Gamma |- []F => B but not the sequent Gamma |- F => B In other words, the standard deduction theorem of classical logic has to be modified for temporal (and similar modal) logics. Leslie often refers to this as "temporal logic being evil". Best, Stephan |

**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

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

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