|
COMP 426 Automated Reasoning
|
| Fall 2004 |
| Brigitte Pientka |
| Time: Tuesdays and Thursdays 11:35am - 12:55pm |
| Location: MMDHAR G-01 (MacDonald Harrington Building) |
This course is designed to provide a thorough introduction to modern constructive logic, its numerous applications in computer science, and its mathematical properties. Some of the topics to be covered are intuitionistic logic, inductive definitions, functional and logic programming, type theory, theorem proving, model checking.
If you are interested, send me e-mail (bp at cs.mcgill.ca).
Prerequisites: This is an upper-level undergraduate course. Prerequisites: COMP 424 or COMP 302 with MATH 340. Please send me e-mail, if you do not fullfill the prerequisites.
| Lectures | TuTh 11:35-12:55, MMDHAR G-01, Brigitte Pientka |
|---|---|
| TA |
Ahmer Ahmedani (Teaching Assistant) aahmed12@cs.mcgill.ca |
| Office Hours |
Wed 2:00-3:00, McC. Room 205N, Brigitte Pientka Tue 10:00-11:00, McC. Room 234, Ahmer Ahmedani (Teaching Assistant) |
| Textbook |
Automated Theorem Proving Frank Pfenning. Course notes Copies will be available here for students. |
| Credit | 3 units |
| Grading | 30% Homework, 20% Midterm, 25% Project 25% Final |
| Homework |
Weekly homework is assigned each Thursday and due the following Thursday. Late homework will be accepted only under exceptional circumstances. |
| Project |
Project topics will be selected after the midterm. Projects consist of an implementation of a theorem prover or decision procedure. The final project requires an implementation in SML and a project report. |
| Midterm |
Tuesday, 19th Oct. Closed book, one sheet of notes permitted. |
| Final |
Thursday 9th Dec.14:05pm - 16:55pm, WONG 1050 Closed book, one sheet of notes permitted. |
| Academic integrity | McGill University values academic integrity. Therefore all students must understand the meaning and consequences of cheating, plagiarism and other academic offenses under the Code of Student Conduct and Disciplinary Procedures (see http://www.mcgill.ca/integrity for more information). Most importantly, work submitted for this course must represent your own efforts. Copying assignments or tests from any source, completely or partially, or allowing others to copy your work, will not be tolerated. |
| Topics |
Natural Deduction, Sequent Calculus, Proof terms, Type checking, Theorem proving, Unification, Redundancy elimination techniques, Functional and Logic Programming, Open problems and applications |
| Home | http://www.cs.mcgill.ca/~bpientka/courses/atp-04/ |
[ Home | Schedule | Assignments | Handouts | Software | Overview ]
bp@cs.mcgill.ca
Brigitte Pientka