CS 4860 
Applied Logic 
Fall 2010 
OverviewThis 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. Instructor: Robert Constable Time: Tue/Thu 10:1011:25am Location:

Announcements 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. 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. 
Administration 
Resources
