1.1 Propositional Axioms and Inference Rules

The proof system uses a number of the propositional axioms suggested by Rosner and Pnueli but also includes our own axioms and inference rules for the operators and chop-plus.

All substitution instances of valid propositional PTL
chop-free temporal logic formulas for finite time
(f ; g) ; h f ; (g ; h) ChopAssoc
(f f1) ; g (f ; g) (f1 ; g) OrChopImp
f ; (g g1) (f ; g) (f ; g1) ChopOrImp
empty ; f f EmptyChop
f ; empty f ChopEmpty
(f f1) (g g1) (f ; g) (f1 ; g1) BiBoxChopImpChop
w w StateImpBi
f ⊃¬¬f NextImpNotNextNot
(f f) f f BoxInduct
f+ f (f more) ; f+ ChopPlusEqv
f g, f ⇒ ⊢ g MP
f ⇒ ⊢ f BoxGen
f ⇒ ⊢ f BiGen

Instead of ChopPlusEqv one can use

fempty (f more) ; f ChopStarEqv

Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023