Computational Logic

Three credits · Graduate

This course focuses on automated theorem proving. We start with a rigorous treatment of propositional and first order calculus (with equality) and the method of natural deduction, giving a thorough investigation of the soundness and completeness proofs and decidability. Then we compare and contrast several automated theorem proving methods such as tableau, resolution, sequent style calculus and rewrite systems. Extensions to other logics will be discussed. Students will implement one of the automated theorem proving methods. Three credits.