7 Axiom system for PITL with finite time

Substitution instances of conventional (nonmodal) tautologies Taut
(f ⌢ g) ⌢ h f ⌢ (g ⌢ h) FChopAssoc
(f0 f1) ⌢ g (f0 ⌢ g) (f1 ⌢ g) FOrChopImp
f ⌢ (g0 g1) (f ⌢ g0) (f ⌢ g1) FChopOrImp
empty ⌢ f f FEmptyChop
f ⌢ empty f FChopEmpty
w w FStateImpBf
(f0 f1) (g0 g1) (f0 ⌢ g0) (f1 ⌢ g1) FBfAndBoxImpChopImpChop
f empty (f more) ⌢ f FChopStarEqv
f f FNextImpWeakNext
f (f f) f FBoxInduct
f g, f ⇒ ⊢ g FMP
f ⇒ ⊢ f FBfGen
f ⇒ ⊢ f FBoxGen

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