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