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
(CP2005), pages 578592, 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 realtime 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), 5795, 1987.

Characterizing Diagnosis and Systems, J. de Kleer, A.K. Mackworth, and R. Reiter.
In Readings in Model Based Diagnosis, 5465, 1992.
Also in
Artificial Intelligence, Volume 56, Issues 23, August 1992, Pages 197222.
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 (41145).
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 FazelZarandi)
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. PatelSchneider (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.
 FOLSWRL: An extension of SWRL to full firstorder logic.
Mar 16 Resolution Strategies and KB Partitioning. Resolution vs. Search Slides (Anya Tafliovich), Partitionbased Logical Reasoning Slides (IJCAI03 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.225275. 2000.

Practical PartitionBased 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 Firstorder DPLL Theorem Proving. Firstorder 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:

DLFOL Reasoner. Online reasoner for DL and FOL (supports OWL DL and includes DL taxonomy viewer).
Apr 20 Answer Set Programming.
ASP Slides (Sheila McIlraith).
Project Presentations