| Lectures | TuThu 11:35-12:55, Trottier 0070 Brigitte Pientka (bpientka@cs.mcgill.ca) |
|---|---|
| TA | Gheorghe Comanici ( gheorghe.comanici@mail.mcgill.ca ) Kamal Al-Marhoobi ( kalmar at cs.mcgill.ca ) |
| Office Hours |
Tue 1:00-3:00, McC. Room 107N, Brigitte Pientka Fr 1:00-3:00, McC. Room 107, Gheorge Comanici Mo 1:00-3:00, McC. Room 108, Kamal Al-Marhoobi |
| Textbook |
Constructive Logic Frank Pfenning. Course notes Automated Theorem Proving Frank Pfenning. Course notes We will make more specific handouts available on WebCT. |
| Credit | 3 units |
| Grading | 30% Homework, 25% Midterm I, 25% Midterm II, 20% Project |
| Homework |
There will be 6 small homeworks which include theoretical and
practical exercises. You have 2 late days you can use throughout the semester. You must however notify the instructor BEFORE the homework is due that you intend to use one or two late days. If you have used up your late days, we will not accepted late homeworks. |
| Midterm |
Thu Feb 12, Midterm I Closed book, one sheet of notes permitted. Thu Mar 26, Midterm II Closed book, one sheet of notes permitted. |
| Projects |
To be announced 3% project proposal, 6% Project milestone, 5% presentation, 6% 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 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/comp527 |