Specification and Verification

Three credits · Graduate

A treatment of formal logic with applications to computer science, starting with a rigorous discussion of propositional and predicate logic (with equality) and culminating in proofs of soundness and completeness. Several automated theorem proving methods such as semantic tableaux, natural deduction, and resolution will be compared. Extensions to other logics will be discussed. Three credits.