ITL
© 1996-2018







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
Note: f ¬¬f (Weak next)
Table 4: Axiom system for PITL with just finite time







2018-10-21
Contact | Home | ITL home | Course | Proofs | Algebra | FL