SE212 Study Guide - Proof Theory, Conjunctive Normal Form, Disjunctive Normal Form

• School: University of Waterloo
• Department: Software Engineering
• Course: SE212
• Professor: Nancy Day

Document Summary

A logic consists of syntax syntax: a format for inscribing the logic semantics semantics: the de nition of validity within the logic and proof theories proof theories: methods of determining validity. The semantics tells us which of these w s are true or valid. Valid formulas are given the symbol (cid:96), and non-valid formulas are marked as (cid:54)(cid:96). When we describe a formula as being proven by theory, we use (cid:15) ; if this is a natural deduction, we use (cid:15)n d. Proof theories do mechanical manipulations on strings or symbols. It does not make use of the meanings of characters, but simply uses them as strings of characters. Semantics and proof theories are related by soundness and completeness. A proof theory is sound if there is a way to prove it that ensures its validity, ie (cid:15) = (cid:96).