ITL
© 1996-2018







16 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-02-26
Contact | Home | ITL home | Course | Proofs | Algebra | FL