Santa Clara University, Spring 2011
COEN 260 Truth Deduction and Computation
Professor: Valeria de Paiva (PhD Cantab)
Lectures: MW 7:10-9:00 Room 106 Bannan
BOOK: Language, Proof and Logic,
John Barwise, John Etchemendy
University of Chicago Press
Catalog Description: Introduction to mathematical logic and semantics of languages for the computer scientist. Investigation of the relationships among what is true, what can be proved, and what can be computed in the formal languages for propositional logic, first order predicate logic, elementary number theory, and the type-free and typed lambda calculus. Prerequisite: COEN 19 or AMTH 240 and COEN 70. (4 units)
WARNING NOTE ON BOOK: WARNING! Do not buy a used copy of the text! The copy of the software that comes with the book can only be registed once. If you cannot register the software, you cannot submit solutions to homework exercises of take-home exam problems or have the correctness of your solutions automatically checked for you prior to submitting them.
HOMEWORK/QUIZZES: Each week, there will be either a homework assignment due or a quiz. In addition, there will be a midterm exam and a final exam. Each exam will consist of an (open-book, open-notes) take-home part and a (closed-book, closed-notes) in-class part.
TOPICS TO BE COVERED:
1. What is Computational Thinking? How does logic fit into it? (1 lecture):
2. Propositional Logics (7 lectures):
• The syntax and semantics of propositional logics
• The logical connectives.
• Building truth tables to test formal validity, both "by hand" and using Boole.
. The distinction between implication and implicature
. "Fitch" and formal proofs.
3. First-Order Logics (7 lectures):
• The syntax and semantics of first-order logics
• Expressing yourself in first-order logics
• Building structures to demonstrate formal invalidity, by hand and using Tarski's World
• Constructing formal deductions to demonstrate formal validity, by hand and using Fitch
4. Lambda-Calculus (3 lectures):
• The syntax and semantics of lambda-calculus, typed and untyped. Curry-Howard isomorphism.
• A quick look at some real-world tools for applying higher-order logics to software engineering problems
5. Modal Propositional Logics (1 lecture):
• The syntax and semantics of temporal, dynamic, and general modal propositional logics
6. Wrap-up (1 lecture):
• Special emphasis on the question of how much support a formal derivation of a proposition provides for believing it to be true