COT 3420 Logic for Computer Science Spring 2003 Mondays and Wednesdays, 12:30-1:45, ECS 138

Instructor

• Geoffrey Smith
• ECS 320
• 305 348-6037
• E-mail: smithg @ cs.fiu.edu
• Office Hours: Mondays and Wednesdays, 11:00 -- 12:00, 2:00 -- 3:00
  I'll usually be happy to meet at other times. Send email, call, or drop by.

Textbook

• Logic in Computer Science: Modelling and reasoning about systems by Michael Huth and Mark Ryan (Cambridge, 2000).

Course Description

Anyone who uses computers much will quickly realize that most computer software doesn't work very reliably. An illustration is offered by the following (quite typical) software disclaimer:

THE SOFTWARE IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, AND WE EXPRESSLY DISCLAIM ALL IMPLIED WARRANTIES, INCLUDING BUT NOT LIMITED TO THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. WE DO NOT WARRANT, GUARANTEE, OR MAKE ANY REPRESENTATIONS REGARDING THE USE OR THE RESULTS OF THE USE OF THE SOFTWARE OR ANY ACCOMPANYING WRITTEN MATERIALS IN TERMS OF THEIR CORRECTNESS, ACCURACY, RELIABILITY, CURRENTNESS, OR OTHERWISE. THE ENTIRE RISK AS TO THE RESULTS AND PERFORMANCE OF THE SOFTWARE AND WRITTEN MATERIALS IS ASSUMED BY YOU.

In this course, we will study mathematical logic. But this is not a mathematics course---our goal here is to apply logic to make us better computer scientists. One application will be to use logic to specify precisely what we want our programs to do. More dramatically, we will develop a logical methodology that can actually lead us to derive correct programs systematically, rather than by trial and error. In general, we will explore a number of logics that help us to analyze and to understand computer programs.

Course Outcomes

Upon successful completion of COT 3420, students will

1. Master reasoning abstractly from formal definitions and specifications using propositional and predicate logic.
2. Master deriving formal proofs using the axioms and rules of inference of a logic.
3. Be exposed to basic concepts of logics, such as soundness and completeness.
4. Be familiar with applications of logic to computer science, such as logic programming or program derivation using Hoare logic.

Approximate Course Structure

1. Propositional Logic
2. Predicate Logic
3. Hoare Logic---we will define the meaning of a small programming language by giving logical rules for each construct.
4. Program Derivation---we will use Hoare Logic to help us to develop programs hand in hand with proofs of correctness.
5. Other Logics---as time permits, we will consider other logics, such as CTL, a logic for reasoning about concurrent systems.

Homework and Grading

I will ask you to form groups of two or three students for the purposes of submitting homeworks; I'll assign homeworks every couple of weeks.

Grades in the course will be determined approximately as follows:

Homeworks	25%
Midterm Exam(s)	25%
Final Exam	45%
Class Participation	5%

Other Matters

Academic Integrity: I expect you to maintain a high level of academic integrity in this course. The basic principle to follow is that the work that you submit should be the result of your group's own effort. You are allowed to consult the web or other books in solving homework problems, or to discuss the problems with other groups, but you must cite any such sources that you use. And you must write up your solutions on your own. It is definitely not acceptable to merely copy answers from other groups, books, or from the Web.

Incompletes: I will grant incompletes only in extreme circumstances, such as medical emergencies.

Attendance: I expect you to attend class regularly and promptly, and to participate in discussions. Please don't be shy about asking questions--if something is unclear to you, it is probably unclear to others as well.

• COT 3420 home page
• Geoffrey Smith's home page