CS81 Computability and Logic

Spring 2012

Syllabus

An introduction to some of the mathematical foundations of computer science, particularly logic, automata, and computability theory. Develops skill in constructing and writing proofs, and demonstrates the applications of the aforementioned areas to problems of practical significance.

Lecture:

MW 14:45-16:00, Jacobs B134

Staff:

Instructor: Christino Tamon (Olin 1241, x-70443)
Grutors: Matthew Johnson, Sarah Johnson, Jordan Librande, Matthew Prince, and Matthew Toal

Office hours:

C. Tamon (Olin 1241): MW 10-11am, TR 2-3pm
Grutors (Platt Living Room):
- Sun 8-10pm (Matt Johnson)
- Mon 8-10pm (Matt Prince), 10pm-12am (Matt Toal)
- Tue 8-10pm (Sarah Johnson), 10pm-12am (Jordan Librande)

Textbooks

M. Huth, M. Ryan, Logic in Computer Science, 2nd edition, Cambridge University Press, 2004. ISBN 0-521-54310-X.
E. Rich, Automata, Computability, and Complexity: Theory and Applications, Prentice-Hall, 2008. ISBN 0-13-228806-0.

Goals

By the end of the course, you should be able to (among other things):

Learn and use new formal systems;
Understand the correspondence between formal logic and natural language proofs;
Write clear and logically valid proofs;
Read and write regular expressions, context-free and unrestricted grammars;
Reason about code using preconditions, postconditions, and loop invariants;
Recognize when regular expressions, context-free grammars, and computations will and will not work for specific problems;
Explain how to translate among regular expressions, nondeterministic finite automata, and deterministic finite automata;
Explain the Church-Turing thesis and list models of universal computation;

Grading

Homework (50%). Midterm (20%). Final exam (30%).

Responsibilities

Attendance

Not mandatory but you are resposible for any material or activities covered in class.

Announcements

Any course announcements will be given in class or via the course emailing list. You are responsible to read the course mailing list.

Late Policy

You have five late days that can be used to extend homework assignments across the semester. No other extensions will be allowed unless requested by the dean.

Collaboration

You are encouraged to discuss any course material with your fellow students but any submitted work must ultimately be your own. Any help you received on your submitted work must be acknowledged. You should come away from any discussion with your fellow students with a real understanding (and not a documented softcopy or hardcopy solution provided by someone else). Any discussion you have on the homeworks should take place on an equal basis (neither receiving complete answers nor giving away complete answers).

Course Schedule:

Week	Date	Topic	HWs	Notes
1	Jan 18	Introduction	HW1 (TeX)	humor
2	Jan 23,25	Propositional logic (H&R 1.1-1.4)	HW2 (TeX)	fitch.sty
3	Jan 30, Feb 1	Predicate logic (H&R 2.1-2.3)	HW3 (TeX)	Natural-Deduction
4	Feb 6,8	Semantics (H&R 2.4)	HW4 (TeX)	Ex4, First-Order-Logic
5	Feb 13,15	Completeness	HW5 (TeX)	misproof
6	Feb 20,22	Tableaux and Sequents [Buss]; Hoare logic (H&R 4.1-4.4)	HW6 (TeX)	Tableaux (TeX, qtree.sty), Sequent (TeX, bussproofs.sty), Hoare-Logic (TeX, algorithms)
7	Feb 27,29	Regular languages and Finite Automata (Rich 1-7)	HW7 (TeX)	Regular, gastex
8	Mar 5,7	Pumping lemmas for regular languages (Rich 8-10)		Ex8
9	Mar 12,14	Spring break
10	Mar 19,21	Context-free languages and Pushdown Automata (Rich 11-12)		Context-Free Ch11:6,18; Ch12:1
11	Mar 26,28	Pumping lemmas for context-free languages (Rich 13-16)	HW8 (TeX)	Ch13:1,3
12	Apr 2,4	Grammars and Turing Machines (Rich 17,23)	HW9 (TeX)	Turing-Machine Ch17:1,3,5; Ch23:1
13	Apr 9,11	Undecidability (Rich 19-21)	HW10 (TeX)	Reducibility Ch21:1,5,7,9,11,12
14	Apr 16,18	Universal models of computation (Rich 18)
15	Apr 23,25	Parsing and Post's problem (Rich 15,22)		Post-Correspondence-Problem Ch15:1,4; Ch22:2,3,4
16	Apr 30, May 2	No classes
17	May 7, 9	Finals