|
|
|
MATH 524: Logic and Automated Reasoning
Description: The course is an introduction to formal
logic from the computational point of view. Special emphasis will be placed on first-order
number theory and the Incompleteness Theorems of Gödel. Algorithmic techniques aiding the
construction and verification of mathematical proofs will be introduced. Students will
harness these ideas through the creation of multiple software systems implementing theorem provers
and/or proof checkers for various fragments of first-order predicate logic. No previous
experience with computer programming is assumed.
Professor: Robert W. McGrail.
Meetings: Tuesday, 9:30 AM to 12:30 PM in Avery 117.
Text:
A Friendly Introduction to Mathematical Logic by
Christopher C. Leary. Prentice Hall. 1999. ISBN: 0-13-010705-0.
Supplement 1:
Incompleteness: The Proof and Paradox of Kurt Gödel
by Rebecca Goldstein. Atlas Books/W.W. Norton. ISBN: 0-393-05169-2.
Supplement 2:
Clause and Effect: Prolog Programming for the Working
Programmer by William F. Clocksin. Springer-Verlag. ISBN: 3540629718. |
|
Course Policies
Class Meetings: These will be conducted in traditional
lecture style, with time reserved at the beginning of each meeting to review the finer points of
homework problems.
Lab Meetings: The weekly meeting will often be partitioned
into two segments: One major time period to cover logical theory and the other to practice
logic programming in Prolog. The Prolog segment will often take place in the Albee 100
laboratory.
Homework: There will be weekly homework assignments
due one week after the relevant material is covered in class.
Presentation: Each student will make a 20-30 minute presentation of some step on
the road to incompleteness. This will occur during the later stages of the course.
Exams: There are no exams.
Grading: There are only two graded activities that affect
the final grade. The breakdown follows.
- Homework: 80%
- Presentation: 20%
|
Syllabus
- October 3rd: First-order languages, terms, formulas, sentences, and Prolog facts and
queries.
- October 10th: Structures, satisfiability, and Prolog clauses and unification.
- October 17th: Substitutions, logical implication, and Prolog lists.
- October 24th: Deductions, logical axioms, and rules of inference.
- October 31st: Soundness, the Deduction Theorem, and nonlogical axioms.
- November 7th: Completeness and compactness.
- November 14th: Recursive sets and recursive functions.
- November 21st: Coding, Gödel Numbers, NUM, and SUB.
- November 28th: Recursive definitions, AxiomsOfN, and coding deductions.
- December 5th: The Self Reference Lemma, Gödel's First and Second Incompleteness Theorems.
|
|
|
Accessible Version
Imprint