#### 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 ﬁnite 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) 1,BiGen 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