COEN260 Basics

Santa Clara University, Spring 2011
COEN 260 Truth Deduction and Computation

Professor: Valeria de Paiva (PhD Cantab)
Email: valeria.depaiva@gmail.com
Lectures: MW 7:10-9:00 Room 106 Bannan
BOOK: Language, Proof and Logic,
John Barwise, John Etchemendy
University of Chicago Press
ISBN 157586374X


Cat­a­log De­scrip­tion: In­tro­duc­tion to math­e­mat­i­cal logic and se­man­tics of lan­guages for the com­puter sci­en­tist. In­ves­ti­ga­tion of the re­la­tion­ships among what is true, what can be proved, and what can be com­puted in the for­mal lan­guages for propo­si­tional logic, first order pred­i­cate logic, el­e­men­tary num­ber the­ory, and the type-free and typed lambda cal­cu­lus. Pre­req­ui­site: COEN 19 or AMTH 240 and COEN 70. (4 units)

WARN­ING NOTE ON BOOK: WARN­ING! Do not buy a used copy of the text! The copy of the soft­ware that comes with the book can only be reg­isted once. If you can­not reg­is­ter the soft­ware, you can­not sub­mit so­lu­tions to home­work ex­er­cises of take-home exam prob­lems or have the cor­rect­ness of your so­lu­tions au­to­mat­i­cally checked for you prior to sub­mit­ting them.

HOME­WORK/QUIZZES: Each week, there will be ei­ther a home­work as­sign­ment due or a quiz. In ad­di­tion, there will be a midterm exam and a final exam. Each exam will con­sist of an (open-book, open-notes) take-home part and a (closed-book, closed-notes) in-class part.

TOP­ICS TO BE COV­ERED:

1. What is Computational Thinking? How does logic fit into it? (1 lec­ture):

2. Propo­si­tional Log­ics (7 lec­tures):
• The syn­tax and se­man­tics of propo­si­tional log­ics
• The log­i­cal con­nec­tives.
• Build­ing truth ta­bles to test for­mal va­lid­ity, both "by hand" and using Boole.
. The dis­tinc­tion be­tween im­pli­ca­tion and im­pli­ca­ture
. "Fitch" and formal proofs.

3. First-Or­der Log­ics (7 lec­tures):
• The syn­tax and se­man­tics of first-or­der log­ics
• Ex­press­ing your­self in first-or­der log­ics
• Build­ing struc­tures to demon­strate for­mal in­va­lid­ity, by hand and using Tarski's World
• Con­struct­ing for­mal de­duc­tions to demon­strate for­mal va­lid­ity, by hand and using Fitch

4. Lambda-Calculus (3 lec­tures):
• The syn­tax and se­man­tics of lambda-calculus, typed and untyped. Curry-Howard isomorphism.
• A quick look at some real-world tools for ap­ply­ing higher-or­der log­ics to soft­ware en­gi­neer­ing prob­lems

5. Modal Propo­si­tional Log­ics (1 lec­ture):
• The syn­tax and se­man­tics of tem­po­ral, dy­namic, and gen­eral modal propo­si­tional log­ics

6. Wrap-up (1 lec­ture):
• Spe­cial em­pha­sis on the ques­tion of how much sup­port a for­mal de­riva­tion of a propo­si­tion pro­vides for be­liev­ing it to be true