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.