© 1996-2018

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