| |
| 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, ,…, ⊢ fn−1 ⊃fn ⇒ ⊢ f1 ⊃fn | | ImpChain
| | ⊢ | f1 ≡ f2, ,…, ⊢ fn−1 ≡ fn ⇒ ⊢ f1 ≡ fn | | EqvChain
| | ⊢ | f1,⊢ f2,…,⊢ fn ⇒ ⊢ g, | | Prop
| | where the formula f1 ∧ f2 ∧…fn ⊃g | |
| | is a substitution instance of a propositional tautology | | |
|
| |
Next