**Prerequisites:** CSCE 580

**Meeting time and venue:** TTh 1230-1345 in SWGN 2A19

**Instructor:** Marco Valtorta

**Office:** Swearingen 3A55, 777-4641

**E-mail:**
mgv@cse.sc.edu

**Office Hours:**
TBD, or by previous appointment.

**
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:

- Represent domain knowledge about objects using propositions and solve the resulting propositional logic problems using deduction and abduction
- Reason under uncertainty using Bayesian networks
- 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
- Represent taxonomic and structural knowledge in ontologies

**Homework **

Grading policy per assignment

- HW1, due 2011-02-01. Do exercises 9.9, 9.11, 9,12, 9.14, and 9.18 in:
Ann Yasuhara.
*Recursive Function Theory and Logic*. Academic Press, 1971.

Explain the difference between the definition of complete in Section 9.2 and the use of the term complete in section 9.7.

Use Theorem 9.7 in support of this argument: "The propositional calculus does not tolerate inconsistency, and therefore it is a bad candidate for representation of human reasoning." - HW2, assigned 2011-02-17, due 2011-03-17: Do all exercises in chapter 5 [P] except 5.12, 5.15 and 5.16. This is a very long assignment, so please start now.
- HW3, assigned 2011-03-29, due 2011-04-7: Exercises 76, 85, and 86 from Schoening's handout.
- Extra credit homework: prepare a set of slides for the "Directional Resolution: The Davis-Putnam Procedure, Revisited," by Rina Dechter and Irina Rish. Details are in the presentation page on this site. This is due on May 4, 2011 at 5pm. Submit the slides (powerPoint or pdf only) using dropbox.

**Notes **

Introductory lecture

Notes on
student presentations (updated 2011-03-03)

Introductory lecture
from Brachman and Levesque

Notes
about student interests from the first and second class meetings

Notes about the propositional
calculus from the lecture of 2011-11-18,
based on:
Ann Yasuhara. *Recursive Function Theory and Logic*. Academic Press,
1971.

Notes about the propositional
calculus from the lecture of 2011-11-20

Notes about the propositional
calculus from the lectures of 2011-01-20 and 2011-01-25

Notes about the propositional
calculus from the lecture of 2011-01-27,
based on:
Uwe Schoening. *Logic for Computer Scientists*. Birkhauser, 1989.

Notes about the propositional
calculus from the lecture of 2011-02-01

Notes about the propositional
calculus from the lecture of 2011-02-03: Horn clauses.

Notes about the propositional
calculus from the lecture of 2011-02-08: The compactness theorem (proved)
and resolution

Notes about the propositional
calculus from the lecture of 2011-02-10: Examples of propositional
resolution; using the propositional calculus for knowledge representation,
based on Poole and Mackworth, Ch.5.

Local copies of slides for Ch.5 of [P]. Link to authors' website
is given elsewhere on this page.

Notes on AILog and the AILog files from Poole and Mackworth

Notes for sections 5.5-5.7 [P]

Notes from lecture of 2011-02-22, with partial correction of HW1 (exercise 9.14(b) [Yasuhara])

Notes about the predicate calculus from the lecture of 2011-03-15: terms, formulas, and semantics,

Notes about the predicate calculus from the lecture of 2011-03-17: terms, formulas, and semantics, with several worked-out exercises.

Notes about the predicate calculus from the lecture of 2011-03-22: normal forms, with some worked-out exercises.

Notes about the predicate calculus from the lecture of 2011-03-24: normal forms, with some worked-out exercises.

Notes about the predicate calculus from the lecture of 2011-03-29: Herbrand structures.

Notes about the predicate calculus from the lecture of 2011-03-31: Resolution.

Notes about the predicate calculus from the lecture of 2011-04-05: Resolution refutation proofs.

Notes about the predicate calculus from the lecture of 2011-04-07: Resolution refutation proof examples.

Graduate Student Presentations

** The USC Blackboard
**
has a site for this course.

**Some useful links: **