ITL
© 1996-2018







4 Propositional proof system

In Table 7 we list the propositional axioms and rules for ITL.


Table 7: Propositional Axioms and Rules for ITL.
ChopAssoc
(f0 ; f1) ; f2 f0 ; (f1 ; f2)
OrChopImp
(f0 f1) ; f2 (f0 ; f2) (f1 ; f2)
ChopOrImp
f0 ; (f1 f2) (f0 ; f1) (f0 ; f2)
EmptyChop
empty ; f f
ChopEmpty
f ; empty f
BiBoxChopImpChop
(f0 f1) (f2 f3) (f0 ; f2) (f1 ; f3)
StateImpBi
p p
NextImpNotNextNot
f ¬¬f
KeepnowImpNotKeepnowNot
keepnow(f) ¬ keepnow(¬f)
BoxInduct
f (f f) f
InfChop
(f inf) ; g (f inf)
ChopStarEqv
f(empty ((f more) ; f))
ChopstarInduct
(inf f (f (g fmore) ; f)) g
MP
f0 f1, f0 ⇒ ⊢ f1
BoxGen
f0 ⇒ ⊢ f0
BiGen
f0 ⇒ ⊢ f0







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