CISC 604: 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, compactness and undecidability. Automated theorem proving also covered.

Current Texts:
Introduction to Mathematical Logic
E. Mendelson
Brooks-Cole/Div. of Wadsworth,Inc.

Logic for Computer Scientists
Uwe Schoning
Birkhauser.
Material from related texts

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, 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 310 or equivalent, or consent of instructor.