1.2 Propositional proofs

Before we prove some theorems, it is worth mentioning a few useful theorems and derived rules. They are all solely based on propositional logic and temporal logic without chop and we omit their proofs.

f1 f2, ,…, fn1 fn ⇒ ⊢ f1 fn ImpChain
f1 f2, ,…, fn1 fn ⇒ ⊢ f1 fn EqvChain
f1,f2,…,fn ⇒ ⊢ g, Prop
where the formula f1 f2 …fn g
is a substitution instance of a propositional tautology

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