[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] LTL axiomatic system
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) )
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.