© 1996-2018

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
(skip f) (skip f) DiSkipImpBiSkip
(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

f empty (f more) ; f ChopStarEqv

(f f1) ; g f ; g AndChopA


f f1 f
(f f1 f)
(f f1 f) (f f1) ; g f ; g
(f f1) ; g f ; g
2, 3,MP

The following related theorem has a similar proof:

(f f1) ; g f1 ; g AndChopB

Contact | Home | ITL home | Course | Proofs | Algebra | FL