University of Toronto - Winter
Department of Computer Science
Topics in KR&R: Automated Reasoning
Course Slides and Readings
Student Paper Assignments and Tips
Preliminary Schedule for Project Presentations
Course Introduction (pdf).
Theorem Proving (pdf b&w) (pdf col) (Scott Sanner).
- Ch. 8&9 of Russell&Norvig 2nd edition (photocopies available in Pratt 283)
SAT and QBF (Fahiem Bacchus).
Combining Component Caching and Clause Learning for Effective Model
Counting, T. Sang, F. Bacchus, P. Beame, H. Kautz, and T. Pitassi,
presented at SAT 2004 9 pages.
Using SAT in QBF,
H. Samulowitz and F. Bacchus, International
Conference on Principles and Practice of Constraint Programming
(CP-2005), pages 578-592, 2005.
Ontology Reasoning with Vampire (Andrei Voronkov).
Model Checking (Marsha Chechik).
- LTL/CTL symbolic (mostly decision diagram) model checkers:
- Model checking for real-time and hybrid systems:
- Combines model checking and theorem proving:
- Explicit state software model checking:
- Symbolic software model checking:
Consequence Finding and Diagnosis. (Sheila McIlraith)
A Theory of Diagnosis from First Principles, R. Reiter. Artificial Intelligence, (32), 57--95, 1987.
Characterizing Diagnosis and Systems, J. de Kleer, A.K. Mackworth, and R. Reiter.
In Readings in Model Based Diagnosis, 54--65, 1992.
Artificial Intelligence, Volume 56, Issues 2-3, August 1992, Pages 197-222.
Supplemental Readings: (Not required reading!)
Algorithms, P. Marquis. In Handbook on Defeasible Reasoning
and Uncertainty Management Systems, D. Gabbay and Ph. Smets
(eds.), Vol. 5 : Algorithms for Defeasible and Uncertain Reasoning,
S. Moral and J. Kohlas (eds.), chapter 2, Kluwer Academic
Publisher, 2000 (41-145).
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)
Additional References: (For those interested.)
- IJCAR Tutorial Slides on DLs , I. Horrocks and U. Sattler.
- Enrico Franconi's DL course web page.
Handbook of Description Logic,
Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, Peter F. Patel-Schneider (Eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press 2003. Talk to Scott or Sheila if you're interested in obtaining a copy of this book.
- OWL Language Reference: The definitive
reference to the OWL language (A DL on the web).
- OWL Language Overview: A more
readable overview of OWL than the language reference.
- SWRL: An extension to OWL to include the specification of rules.
- FOL-SWRL: An extension of SWRL to full first-order logic.
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)
Resolution versus search; Two strategies for SAT I. Rish and R. Dechter. Journal of Automated Reasoning, 24(1/2), pp.225-275. 2000.
Practical Partition-Based Theorem Proving for Large Knowledge Bases, MacCartney, B., McIlraith, S., Amir, E., Uribe, T. IJCAI 2003.
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)
Darwin. Implementation of the Model Evolution Calculus (succeeds FDPLL).
Apr 6 (Ordered) Theory Resolution. Theory Resolution Slides (Christian Fritz), Ordered Theory Resolution Slides (Xing Tan)
DL-FOL Reasoner. On-line reasoner for DL and FOL (supports OWL DL and includes DL taxonomy viewer).
Apr 20 Answer Set Programming.
ASP Slides (Sheila McIlraith).