Computability and Logic

Spring 2005

Instructor: Professor Bob Keller, x 18483, keller@cs.hmc.edu

Catalog Description:

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. Prerequisites: Math 55, Computer Science 60. 3 credit hours. (Both semesters.)

Further Description:

First we’ll look at logic with an emphasis on proofs. We’ll gain some experience in doing proofs in a style known as “natural deduction”, both for propositional and predicate logic. This will be helpful as a way of outlining proofs for the rest of our careers. It is assumed that you’ve seen truth-tabular forms of logic and are already familiar with propositional connectives and quantifiers. This course gives more practice in how to use them in proofs.

We will next examine finite-state automata (computing machines) and their relationship to languages and regular expressions. We’ll look at applications and limitations of these machines, and and then move on to the more powerful pushdown automata.

We will show how pushdown automata exactly characterize the larger family of languages known as context-free languages. These are the languages generated by grammars of the type you studied in CS 60. We’ll look at the applications of these automata, and also show their limitations.

Next we’ll look at Turing machines, which are the most powerful, in some sense. We’ll explore what kind of grammars are equivalent to Turing machines, and along the way, take note of the special subset of context sensitive grammars their specialized Turing machines.

As with other families of machines, even Turing machines have their limitations. However, unlike the others, the limitations of Turing machines can’t be overcome by introducing a more powerful model while staying within what can be realistically computed. In other words, there are problems not solvable by Turing machines or any other family of computing machines. We will show how to prove that certain problems are in this class of unsolvable problems.

Having introduced the necessary theory, we will return to logic and expose a fundamental limitation of logic: that there is no algorithm for determining, in any sufficiently-rich logic framework, whether a statement is or is not true. This in turn implies that such a framework must necessarily be incomplete, that is, there are statements such that neither the statement nor its negation are provable.

Grading: Homework 50%, Exams 50% (2 midterms, 1 final)

Collaboration Policy: No collaboration, unless indicated by the instructor.

Exam Policy: Closed book.

Late Policy: No late work accepted, unless indicated by the instructor.

Text:

James L. Hein: Discrete Structures, Logic, and Computability, 2^nd Edition, Jones and Bartlett, 2002, ISBN 0-7637-1843-2.

Note that we will not “cover” all of the book in this class. The material in this book that is not covered here will likely have been seen in Math 55 or equivalent.

	CS 81 Outline (Draft, 11/29/04)
Day	Topics	Reading
0 (review on your own)	Elementary Notions and Notations: Proof Primer; Sets; Propositional Calculus	1.1-1.2 1.3.1-1.3.2 6.1; 6.2.1-6.2.3
1	Strings and Languages Languages of Logic	1.3.3-1.3.5
2	Formal Reasoning Formal Axiom Systems	6.3 6.4
3	Predicate Logic Equivalent Formulas	7.1 7.2
4	Formal Proofs in Predicate Calculus	7.3
5	Reasoning with Equality Application: Program Correctness	8.1 8.2
6	Higher-Order Logics Lambda calculus Computational Logic (propositional)	8.3 supplement 9.1
7	Computational Logic (predicate) Application: Automated Reasoning Application: Logic Programming	9.2
8	Abstract Data Types as Algebras Relational Algebra Application: Databases	10.1 10.3 10.4
9	Soundness and completeness	supplement
10	Midterm Exam 1
11	Regular Languages and Finite Automata, part 1 Application: Pattern Matching	11.1 11.2
12	Regular Languages and Finite Automata, part 2 Pumping Lemma for Regular Languages Abstract states of a language Myhill-Nerode Theorem	11.3 11.4
13	Context-Free Languages Pushdown Acceptors Application: Language Parsing	12.1 12.2
14	Parsing Techniques, part 1 Normal Forms	12.3
15	Parsing Techniques, part 2 CYK Algorithm	12.3 supplement
16	Pumping Lemma and Other Properties	12.4
17	Midterm Exam 2
18	Turing Machines Church-Turing Thesis Other Turing equivalent models: Markov Algorithms Partial-recursive functions	13.1 13.2
19	Computability The Halting Problem	14.1
20	Reductions Application: “Everyday” Unsolvable Problems Rice’s Theorem	supplement
21	Language Hierarchy Context Sensitive Languages	14.2
22	Complexity Classes	14.3
23	Undecidability of predicate logic	supplement
24	Completeness and incompleteness of predicate logic	supplement
25	Final Exam

Computability and Logic

Application: Logic Programming

Midterm Exam 1

Midterm Exam 2

Final Exam