Re: [tlaplus] LTL axiomatic system

[fl <freder...@xxxxxxxxxxx>]

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