COMP 426: Automated Reasoning
Home : Course Information : Schedule : Assignments : Handouts : Resources

Course Information -- Fall 2007

Lectures MWF 10:35-11:25, Trottier 0070
Brigitte Pientka (
TA TuThu 4:00-5:30 Maja Frydrychowicz (
Office Hours W 2:30-4:00, McC. Room 107N, Brigitte Pientka
Textbook Constructive Logic
Frank Pfenning.
Course notes
Automated Theorem Proving
Frank Pfenning.
Course notes
see also under handouts.
Credit 3 units
Grading 35% Homework, 35% Midterm, 30% Project
Homework There will be 5 small homeworks which include theoretical and practical exercises.
You have 2 late days you can use throughout the semester
Late homework will be accepted only under exceptional circumstances.
Midterm Mo 22 Oct.
Closed book, one sheet of notes permitted.
Projects To be announced
6% project proposal, 4% Project milestone, 10% presentation, 10% final report
the project includes reading and presenting a research paper, providing a small practical implementation together with a final report.
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 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