CS 421 Formal Methods

From Computer Science
Jump to: navigation, search

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.


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)