January 15 (Thu), 2013 Administrative information: resources, syllabus, grading policy. Discussion of student interests and expectations completed. Students are asked to verify that they have access to the blackboard site for the course, where some documents will be uploaded.
January 17 (Thu), 2013 Planning and the situation calculus. Presentation based on Ch.9 [Levesque]. (See course web site for detailed bibliographical information and links to slides and code; see blackboard course site for readings.) Introduction to the state-space approach to planning. Three coins, monkey and bananas example. A simple Prolog-based planned. Examples of code and its execution.
January 22 (Tue), 2013 Program 1 will likely consist of exercises 3,6,7,8 from Ch.9 [Levesque]. This will be confirmed on Thursday. More on planning. Review of some Prolog constructs. The need for bounded plan (bplan) to avoid infinite regress on plans of unknown size. Search and representation issues in realistic planning problems. An approach to deal with the frame problem in planning: the situation calculus. Fluents (started).
January 24 (Thu), 2013 PR1 assigned: Exercises 3,6, and 7 from Ch.9 [Levesque], due on Thursday, January 31. Please turn in a printout with the code and examples of use. The situation calculus and fluents, completed, with the monkey and bananas code described and run. 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, a couple of failed proofs of (A \supset A). A good proof of (A \supset A).
January 29 (Tue), 2013 Discussion of the PR1 exercises, with emphasis on 9.7. Propositional calculus: the deduction theorem.
January 31 (Thu), 2013 PR1 due date changed to Tuesday, February 5. The propositional calculus: proof of the converse of the deduction theorem, some syntactic proofs, semantics of the propositional calculus, equivalent formulas, the substitution theorem (statement and example).
February 5 (Tue), 2013 PR1 collected. Exercise 9.7 will not be counted for credit. The propositional calculus. Exercises in section 9.5: 9.9 (c) and (d); 9.11, 9.12, 9.14. Proof of soundness and consistency of the propositional calculus.
February 7 (Tue), 2013 HW1 assigned: Exercise 9.19 [Yasuhara], due on Thursday, February 14. The propositional calculus: proof of (Post-)completeness of the propositional calculus.
February 12 (Tue), 2013 The compactness theorem (proved following: Donald W. Loveland, Automated Theorem Proving: A Logical Basis, North-Holland, 1978, theorem 1.6.1. First-order logic: axiomatic presentation (five axioms, two rules of inference). Conjunctive normal form (CNF), propositional case. Resolution, started.
February 14 (Thu), 2013 HW1 collected, but returned for further work: the students are encouraged to write down the proof of the simplified version proved in class and fill in the details of the proof sketch presented in class. Suitable assignments, models, logical consequence. Presentation based on Ch.1 of: Uwe Schoening. Logic for Computer Scientists. Birkhauser, 1989.
February 19 (Tue), 2013 HW1 collected. Normal forms, with example of conversions. Propositional resolution.
February 21 (Thu), 2013 PR1 and HW1 graded and returned to some at end of class. HW2 assigned. Do exercise at the end of notes for today's class. Horn clauses, in the propositional case. Schoening's marking algorithm for Horn formula satisfiability.
February 23 (Thu), 2013 PR1 and HW1 returned. HW2 collected. HW2 correction done in class. Predicate logic, following Schoening: well-formed formulas, definition of structure (a.k.a. interpretation) with examples. Another example of propositional resolution.
February 28 (Thu), 2013 MT1.
March 5 (Tue), 2013 Correction of MT1 in detail.
March 7 (Thu), 2013 Discussion of student project (with team assignments) and of student paper presentations. More information will be placed on the course web site.
March 19 (Tue), 2013 Discussion of student paper presentations. Semantics of predicate logic (following Schoening, mostly).
March 21 (Thu), 2013 HW3 assigned: do exercises 56 and 57 in Ch.2 [Schoening]. Semantics of predicate logic, with some applications.
March 28 (Thu), 2013 (March 26 lecture was not given, due to travel to University of Aalborg.) HW3 collected and discussed. Semantics of predicate logic and normal forms.
April 2 (Tue), 2013 Discussion of new grading scheme (including project). Schedule of presentations: 4/16 (Tuesday): Aikju and Sakhib; 4/18 (Thursday): Omar and Walker; 4/23 (Tuesday): McCaslin and Salvi. Semantics of predicate logic and normal forms: Skolemization. Yingke Chen's dissertation ("Machine Learning-based Verification: Informed Learning of Probabilsitic System Models"): presentation started; Chen's slides are on blackboard.
April 4 (Thu), 2013 Discussion of new grading scheme (including project): update. Summary example of conversion of a predicate calculus formula to clausal CNF. Yingke Chen's dissertation ("Machine Learning-based Verification: Informed Learning of Probabilistic System Models"): most of the presentation done; Chen's slides are on blackboard.
April 9 (Tue), 2013 HW4 assigned: exercise 78 [Schoening]. Herbrand's Theory (Section 2.4 [Shoening]); the Unification Algorithm (first part of Section 2.5 [Schoening]).
April 11 (Thu), 2013 HW5 assigned: exercise 85 [Schoening]. HW4 corrected and discussed in class. Examples of resolution refutation proofs.
April 16 (Tue), 2013 HW6 assigned: complete proof of existence of right-inverse; concentrate especially on the substitution in the first step of the proof. HW3 and HW4 returned, graded. A resubmission, due on Thursday, was requested. HW5 was not collected; it will be collected on Thursday. Discussion of HW5. More examples of resolutution proofs. First graduate student presentation will be on Thursday.
April 18 (Thu), 2013 HW5 (dragons exercise, exercise 85 [Schoening]) discussed in class in detail. Presentation by Hanin Omar and Richard Walker on Directional Resolution.
April 23 (Tue), 2013 The next class will start at 9am. Conclusion of presentation by Hanin Omar and Richard Walker on Directional Resolution, including a comparison of the original DP algorithm (directional resolution) and DPLL. Presentation by Rhea McCaslin and Dhaval Salvi on Knowledge Representation and Question Answering.
April 25 (Tue), 2013 Presentation on Description Logics by Jahan Arju and Nazmus Sakib. An introduction to Bayesian networks. Student evaluation of course.