Reference: propositional inference rules 2.28 2002/03/07 2009/01/07 12:46:55.069 US/Central Ian Barland ibarland@radford.edu John Greiner greiner@cs.rice.edu Phokion Kolaitis kolaitis@cse.ucsc.edu Moshe Vardi vardi@cs.rice.edu Matthias Felleisen matthias@ccs.neu.edu Ian Barland ibarland@radford.edu John Greiner greiner@cs.rice.edu Elim inference rule Intro propositional logic A set of inference rules for propositional logic Our propositional inference rules Abbreviation Name If you know all of… …then you can infer ∧Intro and-introduction φ ψ φ ψ ∧Elim and-elimination (left) φ ψ φ and-elimination (right) φ ψ ψ ∨Intro or-introduction (left) φ φ ψ or-introduction (right) ψ φ ψ ∨Elim or-elimination φ ⊢ θ ψ ⊢ θ φ ψ θ ⇒Intro if-introduction φ, ψ, …, θ ⊢ ω φ ψ … θ ω ⇒Elim if-elimination (modus ponens) φ ψ φ ψ Intro false-introduction φ φ Elim false-elimination φ RAA reductio ad absurdum (v. 1) φ ⊢ φ reductio ad absurdum (v. 2) φ ⊢ φ ¬Intro negation-introduction φ φ ¬Elim negation-elimination φ φ CaseElim case-elimination (left) φ ψ φ ψ case-elimination (right) φ ψ ψ φ As usual, φ, ψ, θ, ω are meta-variables standing for any WFF. This is by no means the only possible inference system for propositional logic. This set of inference rules is based upon Discrete Mathematics with a Computer by Hall and O'Donnell (Springer, 2000) and The Beseme Project.