CSCE 781: Knowledge Systems (Spring 2013)

This site is under construction

Prerequisites: CSCE 580

Meeting time and venue: TTh 930-1045 in SWGN 2A18

Instructor: Marco Valtorta
Office: Swearingen 3A55, 777-4641
E-mail: mgv@cse.sc.edu
Office Hours: TBD, or by previous appointment.

Syllabus

Grading and Program Submission Policy

Reference materials: No textbook is required for this course. Readings and notes will be used. Here are some key resources:

David Poole and Alan Mackworth. Artificial Intelligence: Foundations of Computational Agents. Cambridge University Press, 2010. (referred to as [P]) The full book with slides, etc. is available online.

David Stuart Russell and Peter Norvig. Artificial Intelligence: A Modern Approach. Prentice-Hall, 2003 ( [AIMA] or [R] or [AIMA-2]; a third edition is also available).

Ronald Brachman and Hector Levesque. Knowledge Representation and Reasoning. Morgan-Kaufmann, 2004.

Frank van Harmelen, Vladimir Lifschitz, and Bruce Porter (eds.). Handbook of Knowledge Representation. Elsevier, 2007.

Hector J. Levesque. Thinking as Computation: A First Course. MIT Press, 2012. Supplements, including a full set of slides are available online.

Uwe Schoening. Logic for Computer Scientists. Birkhauser, 1989.

Ann Yasuhara. Recursive Function Theory and Logic. Academic Press, 1971.

• Represent domain knowledge about objects using propositions and solve the resulting propositional logic problems using deduction and abduction
• Represent domain knowledge about individuals and relations in first-order logic
• Do inference using resolution refutation theorem proving
• Represent knowledge in Horn clause form and use Prolog (or a dialect thereof) for reasoning
• Represent knowledge for specialized task domains, such as diagnosis and troubleshooting

Homework

Final Project

Notes
Introductory lecture
Notes about student interests from the first meeting
The Monkey and Bananas problem represented using the situation calculus
Notes on the propositional calculus (2013-01-31): proof of the converse of the deduction theorem, some syntactic proofs, semantics of the propositional calculus, equivalent formulas, the substitution theorem (statement and example)
Notes on the propositional calculus (2013-02-05): soundness and consistency of the propositional calculus.
Notes on the propositional calculus (2013-02-07): completeness of the propositional calculus.
Notes on the propositional calculus (2013-02-12): the compactness theorem. Axiomatic presentation of the (first-order) predicate calculus ("first-order logic"), with five axioms and two rules of inference. Conjunctive normal form (CNF), propositional case. The resolution rule (propositional case; started).
Notes on the propositional calculus from the lecture of 2013-02-14.
Notes on the propositional calculus (normal forms, propositional resolution) from the lecture of 2013-02-19.
Notes on the propositional calculus (normal forms, propositional resolution, Horn formulas) from the lecture of 2013-02-21. Note: this includes the notes from 20130219.
Another example of proof by resolution refutation from the lecture of 2013-02-26. Note: this includes the notes from 2013-02-19 and 2013-02-21.
Notes used in the lecture of 2013-03-05, including MT1 correction.
Notes used in the lecture of 2013-03-07, on the semantics of the predicate calculus and on the student project and presentations.
Notes used in the lecture of 2013-03-19, on the semantics of the predicate calculus.
Notes used in the lecture of 2013-03-21, on the semantics of the predicate calculus.
Notes used in the lecture of 2013-03-28, on the semantics of the predicate calculus and normal forms.
Notes used in the lecture of 2013-04-02, on Skolemization, a revised grading scale, and a schedule of student presentations.
Notes used in the lecture of 2013-04-04, with a summary example of conversion to clausal CNF, as will be used for resolution in the predicate calculus case. (These notes include the notes from 2013-04-02.)
Slides for FOL resolution refutation. used (partly) on 2013-04-09.
Notes used in the lecture of 2013-04-11, with a few examples of resolution refutation proofs, including an example in which either non-binary resolution (as presented in Schoening) or factoring is needed.
Notes used in the lecture of 2013-04-16, with an example of a resolution proof from group theory.
Notes on Bayesian networks used in the lecture of 2013-04-25.

Graduate Student Presentations

Lecture Log

The USC Blackboard has a site for this course.

Prolog Information

Some useful links: