CISC 404: Logic in Computer Science

Catalog Description:
Formal introduction to first-order logic with emphasis on its relevance to computer science. Syntax, semantics, models, formal proofs and results on soundness, consistency, completeness, and compactness. Automated theorem proving also covered.

Current Texts:
Introduction to Mathematical Logic, 4th edition
E. Mendelson
Chapman & Hall, London, 1997.

Logic for Computer Scientists
U. Schöning
Birkhäuser Boston, 1989

Goals:
This course introduces formal first-order logic with emphasis on its applications in computer science. It should prepare graduate students for more advanced courses in theoretical computer science, data bases, artificial intelligence and logic programming.

Contents:

• Propositional Logic: syntax, semantics, and proof methods.
• First-order logic: syntax, semantics, models, formal proofs, soundness, consistency, completeness, and compactness, undecidability of first-order logic, Herbrand's theorem and resolution-based automated theorem proving.
• Additional topics, as time permits, to be chosen from: Horn clauses and logic programming, extensions of first-order logic (modal logic, higher-order logic), Gödel's incompleteness theorem, Löwenheim-Skolem theorems, and definability.

Required Background: CISC 301 or 310 or equivalent, or consent of instructor.