ITL
© 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


Proof:

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

The following related theorem has a similar proof:


(f f1) ; g f1 ; g AndChopB








2018-02-26
Contact | Home | ITL home | Course | Proofs | Algebra | FL