CS 4860

Applied Logic

Fall 2010



This is a course on logic, from the point of view of Computer Science. The driving idea is to use CS background as a lens to look deeply into parts of logic by viewing them in CS terms. The course will focus on aspects of logic that are used in formal methods, an area of CS concerned with how to specify programming tasks and demonstrate that programs and protocols are correct according to their specifications. This area of computer science is critical to computer security, a topic of intense interest to industry and government and one that requires solid knowledge of applied logic.

Topics covered include propositional calculi, predicate calculi, programming logics, Hoare logic, program verification, interactive proof assistants, model checking and other topics in formal methods.


Robert Constable
4147 Upson Hall
Office Hours: Tue and Thu 1:30-2:15 and by appointment.

Time: Tue/Thu 10:10-11:25am




 In Class Quiz: October 28th (about the Completeness Theorem)

In Class Quiz: Thursday, November 11th. The topic will be induction proofs, the least number principle, and the computational meaning of induction.

Announcement for Homework Assignment 6:

Problem 5 Explain how to implement the Least Number Principle as a while rule in the style of Hoare's while rule.

Assume that the relation we are proving, R(x) is decidable in the sense that we can prove All x:N.(R(x) or not R(x)) without using the law of excluded middle, P or not P.

Final Quiz on December 2nd in Class


REMINDER There will be a final in class quiz on the semantics of evidence (propositions as types, proofs as terms, etc.) on Thursday December 2.

There is a small typo in Problem 5 of Problem Set 7 that is corrected in the current posting.
Problem Set 7: Another typo corrected today (12/2/10)

The problem should use the predicate OnList(x,l) not On(x,l).


The Final Project for the course is due at the end of study week, Wed December 8 with possible extensions by request to Friday December 10.