University of Toronto - Winter 2006
Department of Computer Science

CSC 2542: Topics in KR&R: Automated Reasoning

Course Slides and Readings



Student Paper Assignments and Tips
Preliminary Schedule for Project Presentations



Jan 12 Course Introduction (pdf).

Jan 19 Theorem Proving (pdf b&w) (pdf col) (Scott Sanner).

Jan 26 SAT and QBF (Fahiem Bacchus).

Feb 1 Ontology Reasoning with Vampire (Andrei Voronkov).

Feb 2 Model Checking (Marsha Chechik).

Feb 9 Consequence Finding and Diagnosis. (Sheila McIlraith)

Feb 16 Planning. Compilation of Planning to SAT (Yiqiao Wang), Recent Trends in Planning (Ali Akhavan Bitaghsir), Administrative Notes

Feb 23 Reading Week -- No Class.



Mar 2 Knowledge Compilation. Horn Theory Approximation Slides (Kelvin Ku), Knowledge Compilation Map Slides (Adnan Darwiche)

Mar 9 Description Logics. FaCT Tableau Algorithm Slides (Sebastian Mieth), Optimising DL Subsumption Slides (Maryam Fazel-Zarandi)

Mar 16 Resolution Strategies and KB Partitioning. Resolution vs. Search Slides (Anya Tafliovich), Partition-based Logical Reasoning Slides (IJCAI-03 Talk Slides, presented by Arnold Binas)

Mar 23 Generalizing Boolean Satisfiability. Part I Slides (PPT) (PDF) (Abida Raouf), Part II Slides (Jessica Davies)

Mar 30 First-order DPLL Theorem Proving. First-order DPLL Slides (Stavros Vassos), Model Evolution Calculus Slides (Jorge Baier)

Apr 6 (Ordered) Theory Resolution. Theory Resolution Slides (Christian Fritz), Ordered Theory Resolution Slides (Xing Tan)

Apr 20 Answer Set Programming. ASP Slides (Sheila McIlraith).

Project Presentations