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).
Readings:
- Ch. 8&9 of Russell&Norvig 2nd edition (photocopies available in Pratt 283)
Jan 26
SAT and QBF (Fahiem Bacchus).
Readings:
-
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.
Feb 1
Ontology Reasoning with Vampire (Andrei Voronkov).
Feb 2
Model Checking (Marsha Chechik).
Software Links:
- 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:
Feb 9
Consequence Finding and Diagnosis. (Sheila McIlraith)
Readings:
-
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.
Also in
Artificial Intelligence, Volume 56, Issues 2-3, August 1992, Pages 197-222.
Supplemental Readings: (Not required reading!)
-
Consequence Finding
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).
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)
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)
Readings:
-
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)
Software Links:
-
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)
Software Links:
-
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).
Project Presentations