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

Re: [tlaplus] LTL axiomatic system

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

Can 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?