Office hours: Monday and Friday 1-2 or by appointment
Grading Policy for 427 :
Midterm
35 %
Final
35 %
Assignments
30 %
Grading Policy for 527 :
Midterm
35 %
Final
35 %
Assignments
20 %
Paper
10 %
Please note that the students enrolled in 527 will have
different midterm and final
Workload for 427:
The undergraduates are expected to do weekly homework assignments and
read approximately 40 pages a week. This will take 12 to 15 hours per
week.
Workload for 527:
The graduates are expected to do weekly homework assignments and read
approximately 40 pages a week.
This will take 12 to 15 hours per week. In addition they are
responsible for writing a term paper.
Description: Logic is the cornerstone of mathematical
reasoning
and it is widely used in computer science.
In addition to formalizing the reasoning rules,
logic also highlights the distinction between formal
manipulation of symbols and their meaning or
interpretations. Even programming can be seen as a logical
activity. To design a program is to prove a proposition
in a constructive manner. To execute a program is to
"normalize" a proof. To find a type of an expression is to
find the proposition of which the expression is a proof.
The notions of logic introduced are basic:
what constitutes a legal argument, how to write correct proofs, how
to use inference systems and how to reason semantically.
Students will be able to apply the knowledge acquired in this class
in the area of software engineering (proving or verifying
properties of programs) and of programming languages (semantics
or type theory).
The course begins with a treatment of
propositional logic. We introduce a proof calculus and a
semantics based on truth tables.
Among all the different systems to describe propositional logic,
Hilbert systems, sequent calculus and natural deduction, we will
study natural deduction. Natural deduction comes as close as possible
to actual reasoning and it allows a close relation to type inference
systems.
We prove soundness and completeness of
propositional logic: the notions of truth and provability coincide.
We will then go into first-order logic and prove again
soundness and completeness. We also establish the undecidability
of first-order logic: there cannot be an algorithm
that decides if a formula is provable or not.
We might conclude the course with a brief introduction to
some current research areas such as logical frameworks, automated
deduction and the Curry-Howards isomorphism.