What you wrote is an axiom for the weak until or unless operator, typically written W, not to be confused with the (strong) until operator denoted by U.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
Hi Frédéric,the axiom system given in the slides that you point to is correct (sound and complete) for LTL. You can also find several variations on LTL proof systems, with different combinations of operators, in our bookFred Kröger, Stephan Merz. Temporal Logic and State Systems. Texts in Theoretical Computer Science, Springer, 2008.
Hi Frédéric,the axiom system given in the slides that you point to is correct (sound and complete) for LTL. You can also find several variations on LTL proof systems, with different combinations of operators, in our book
On 12 Aug 2016, at 12:47, 'fl' via tlaplus <tla...@googlegroups.com> wrote:Hi Frédéric,the axiom system given in the slides that you point to is correct (sound and complete) for LTL. You can also find several variations on LTL proof systems, with different combinations of operators, in our bookCan you prove a theorem likle this one and if not why?( P <=> Q ) ( R <=> S )--------------------------------------------------------------------( ( P until R ) <=> ( Q until S ) )
Why is predicate calculus never explained in slides of the kind mentionned above?
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) )
First-order temporal logic is easy to define semantically, but hard to axiomatize.
On 15 Aug 2016, at 19:41, 'fl' via tlaplus <tla...@googlegroups.com> wrote:First-order temporal logic is easy to define semantically, but hard to axiomatize.
But can we find such a system of axioms somewhere?
On 15 Aug 2016, at 19:29, 'fl' via tlaplus <tla...@googlegroups.com> wrote: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.
LS4 is no longer available apparently.
--
FL
The temporal logic prover `ls4` is available at [1].