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

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

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

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

**Some useful links: **