Outline of CS323

A listing of the topics covered by each class

  1. Logical AI, the background to representing information in logic. An overview of what will be covered in the course, and what homeworks, papers etc. are required.
  2. First order logic, model theory, proof theory. Second order logic, Henkin models. Theorem Provers, PVS.
    Enderton's "A Mathematical Introduction to Logic" provides a good introduction to logic in general. It is a little light on higher order logic, which we will use a lot. However, luckily there is little to know.
    We shall need to use the PVS theorem prover. Using theorem provers is an art, which takes time to learn, but which is very valuable. PVS is actually quite easy to use, after initial teething pains.

  3. The situation calculus and the event calculus: The two main formalisms for reasoning about change.
  4. McCarthy and Hayes. The limitations of the situation calculus. Reiter's foundation axioms, categoricity. Representing actions. Kowalski's event calculus. Linear vs branching time.
    For this class the basic references are McCarthy and Hayes, Some Philosophical Problems from the Standpoint of AI, Knowledge In Action a draft of a book by Ray Reiter. Some contributions to the metatheory of the situation calculus a overview paper by Fiora Pirri and Ray Reiter, and Combining Narratives by John McCarthy and Tom Costello. Event Calculus Revisited by Murray Shanahan.

  5. The frame problem: A major problem of logical AI. Its monotonic solution.
  6. Frame axioms. The Yale Shooting Problem. Hayes's objections. Generating successor state axioms in presence of domain constraints.
    The main papers here are McCarthy and Hayes, Some Philosophical Problems from the Standpoint of AI, Ray Reiter's A simple solution to the frame problem (sometimes).
    Leora Morgenstern has a overview paper on problems with solutions to the frame problem, The Problem with Solutions to the Frame Problem.

  7. Planning and prediction in temporal formalisms.
  8.  Goal regression, implementation in theorem provers. Examples.  Axiomatization of the Blocksworld.  Theory put into PVS.

  9. Non-monotonic reasoning: why we need it? (elaboration tolerance). Various basic forms of circumscription, domain/predicate/formula.  Handout
  10.  Definitions, model theory, soundness and "completeness". Minimal model semantics.

  11. The expressive power of circumscription. The complexity of circumscription.  Handout
  12. Meaning of minimizing a formula. Characterization of expressive power of different variants. NP hierarchy, and complexity.

  13. How to reduce circumscription to first order logic. Two methods, DLS and SCAN.
  14. Pointwise circumscription and Chronological minimization. Handout about action. There were also photocopies of Vladimir's Lifschitz's Pointwise Circumscription paper, and some pages (451-459) from Vol 4. of the Handbook of logic in artificial intelligence. (The chapter by Shoham and Sandewall.)
  15. Domain formula circumscription. Bossu and Seigel and the limit assumption. Handout
  16. Ways of making circumscription satisfiability preserving. Cofinal circumscription. Handout
  17. Circumscription and the frame problem. Solutions by Baker, Lin and Reiter. The projection problem: Solutions by Lin and Reiter, Giunchiglia and Costello.
  18. Splitting theories to reduce casual reasoning to projection, Giunchiglia and Lifschitz.
  19. Non-monotonic consequence relations
  20. Defeasable logic and conditional logic
  21. Default logic and the necessary modifications to make it cumulative.
  22. Auto-epistemic logic
  23. Belief revision as proposed by AGM
  24. Belief update and its relationship to theories of action.
  25. Counterfactuals (McCarthy and Costello, Pearl, Lewis, Stalnaker, Ginsberg's approaches)
  26. Intentional phenomena: Names of formulas and abstract syntax. The paradoxes of syntactic modality. Perlis's and others approach to truth predicates and these paradoxes.
  27. Contexts, lifting axioms. Modal logic approaches to context.

Possible topics for final papers:
T Costello

Last modified: Tue Mar 31 15:17:14 PST 1998