CS 421 Formal Methods
Contents
Catalog Description
Elements of formal logic; various approaches to automation including resolution; restrictions and search methods; inductive theorem-proving; Knuth-Bendix completion; Boyer-Moore theorem-prover; applications. Prerequisite - C or better in CS 202 and CS 303.
Prerequisites
Student must have knowledge of Discrete Structures
Standard Content
Course Outline
This is meant to be a “Logic in Computer Science” course. The main topics covered are Propositional and First Order Logic Syntax and Semantics,proofs of valid arguments via resolution are stressed. Invalidity of arguments is demonstrated through the building of models for the premises and negated conclusions. The use of Automated Reasoning programs such as the OTTER theorem prover and MACE2 model builder is shown. Reasoning with equality , is discussed using equality theories and paramodulation. Reasoning in Inductive Theories is covered. Applications covered are: Program Analysis, Design of Logic Circuits, Plan Generation,Question Answering, Answer Extraction, and Logical Foundations of Databases.
Learning Outcomes
A knowledge of deductive logic and its applications in Computer Science.
Important Assignments and/or Exam Questions
Assignments include chapter summaries of textbook chapters, and use of theorem provers and model builders ; pencil and paper quizzes are given over the course content.
Standard resources
Symbolic Logic and Mechanical Theorem Proving by C-L Chang and R.C.T. Lee (Academic Press, 1973, ISBN-10: 0-12-170350-9)
