**January 13 (Thu), 2011**
Administrative information:
resources, syllabus, grading policy.
How 781 relates to 580 and 780.
Introduction to knowledge representation and reasoning.
General methods in KR&R, classes of knowledge and specialized
representations, KR in applications.
AI as the synthesis and analysis of computational agents that act intelligently.
Agents and environments.
The symbol-system hypothesis (Newell and Simon) and the Church-Turing thesis.
The role of representation in an intelligent agent.
Discussion of student interests and expectations for about half of the students.

**January 18 (Tue), 2011**
Discussion of student interests and expectations completed.
Three different kids of representations, based on: states,
propositions, relations.
The propositional calculus, following the presentation in Ch.9 of: ]
Ann Yasuhara. Recursive Function Theory and Logic. Academic Press, 1971:
Hilbert-style formal system (P_0), syntax, the deduction theorem.

**January 20 (Thu), 2011**
The propositional calculus, following the presentation in Ch.9 of: ]
Ann Yasuhara. Recursive Function Theory and Logic. Academic Press, 1971:
truth tables, soundness of P_0.

**January 25 (Tue), 2011**
HW1 assigned, due on Tuesday, February 1, 2011. (See elsewhere for details.)
The propositional calculus, following the presentation in Ch.9 of:
Ann Yasuhara. Recursive Function Theory and Logic. Academic Press, 1971:
Ccmpleted, including a proof of the completeness of the PC (Lemma 9.2,
Theorem 9.5) and much related discussion.

**January 27 (Thu), 2011**
Suitable assignments, models, logical consequence. Presentation based on
Ch.1 of:
Uwe Schoening. Logic for Computer Scientists.
Birkhauser, 1989.

**February 1 (Tue), 2011**
HW1 collected.
Theorem 9.6 [Yasuhara] proved.
Equivalence, the substitution theorem, CNF, DNF, and 3-CNF following Schoening.

**February 3 (Thu), 2011**
Horn clauses. Efficient satisfiability test for Horn clauses: algorithm
with proof of correctness, following Schoening.

**February 8 (Tue), 2011**
The compactness theorem (proved following: Donald W. Loveland,
*Automated Theorem Proving: A Logical Basis*, North-Holland, 1978,
theorem 1.6.1.
(Binary) resolution in the propositional case. Resolution is
refutation-complete: not proved, stated only.

**February 10 (Thu), 2011**
Examples of resolution refutation proofs.
Methodology used by a knowledge base designer to represent the world using the
propositional calculus, from Poole, section 5.1.

**February 17 (Thu), 2011**
Midterm will be on Thursday, February 24. It will consists of problems similar
to the exercises and example in Yasuhara's ch.9 and Schoening's Ch.1.
HW2 assigned: all exercises in Ch.5 [P], except 5.12, 5.15, and 5.16,
due 2011-03-17.
Poole's Ch.5 through most of section 5.4, with some AILog illustrations.

**February 22 (Tue), 2011**
Midterm will be on Thursday, February 24. It will consists of problems similar
to the exercises and example in Yasuhara's ch.9 and Schoening's Ch.1.
HW1 returned. Discussion of HW1, especially exercise 9.14(b) [Yasuhara].
Conflicts and consistency-based diagnoses;
the top-down consequence-finding procedure modified to find conflicts.

**February 24 (Thu), 2011**
Midterm 1.

**March 1 (Tue), 2011**
MT1 returned. Some discussion of MT1.
Ch.5 AILog examples from [P] through example 5.20 on
consistency-based diagnosis.

**March 3 (Thu), 2011**
Ch.5 AILog examples from [P] completed.
Causal models, following section 5.7 [P].
Discussion of student presentations: five options given; see slides on website.

**March 15 (Tue), 2011**
Foundations of (first-order) predicate logic, following
section 2.1 of:
Uwe Schoening. Logic for Computer Scientists.
Birkhauser, 1989.

**March 17 (Thu), 2011**
HW2 due date is delayed to March 24.
Students are encouraged to choose a paper for presentation.
More on predicate logic, with worked-out exercises.

**March 22 (Tue), 2011**
HW2 due date is March 24.
Discussion of some issues concerning HW2. Some Q&A.
More on predicate logic, with worked-out exercises: normal forms.

**March 24 (Thu), 2011**
HW2 collected.
More on predicate logic, with worked-out exercises: normal forms.
Discussion of undecidability, based on Section 2.3 [Shoening]: there exists
formulas in predicate logic that are satisfiable but have no model of finite
size; proof the validity problem for formulas of predicate logic is undecidable
by reduction of the Post correspondence problem to it (sketch).

**March 29 (Tue), 2011**
HW3 assigned: exercises 76, 85, and 86 from Schoening's handout,
due 2011-04-07.
Herbrand structures.

**April 1 (Thu), 2011**
Resolution refutation for FOL.
All students now have presentations assigned.
The first presentation will be
on April 7, by Hongying Du and Mingzhe Du.

**April 5 (Tue), 2011**
Reminder: HW3 due on Thursday, April 7.
All students now have presentations assigned.
The first presentations will be
on April 12 (Tuesday): by Hongying Du and Mingzhe Du; and by Andrew Smith, etc.
Examples of resolution refutation proofs.

**April 7 (Thu), 2011**
HW3 collected; solution discussed in class.
Datalog, following Poole.
The course Datalog KB.
The west.ail KB, with a recursively defined relation.
First-order version of electrical domain KB.
A KB with functions: before.ail.

**April 12 (Tue), 2011**
Presentation by Jeremy Lewis, Jhih-Rong Lin, and Andrew Smith on
Consistency-Based vs. Explanation-Based (Abductive) Diagnosis.

**April 14 (Thu), 2011**
Final Project handed out. This will be in place of the final exam.
Presentation by Hongying Du and Mingzhe Du on John McCarthy's "Programs with
Common Sense" and by Jordan Bradshaw and Corey White on Complexity of
Terminological Reasoning.

**April 19 (Tue), 2011**
Presentation by Ashok Kumar and Nick Stiffler on "Equipping Robot Control
Programs with First-Order Probabilistic Reasoning Capabilities," by Dominik
Jain, Lorenz Moesenlechner, and Michael Beetz.
End of course student evaluation.

**April 21 (Tue), 2011**
Reminder: Final project is in place of the final exam.
An extra credit assignment is now available---see course web site.
Presentation by Ousmane Dia and Mohamed Sharaf on "Formal Verification of
Sequential Hardware: A Tutorial," by Michael McFarland.
End of course.