COMP4415 Logical Foundations of Artificial Intelligence
This page contains notes from COMP4415 as taught by ron van der Meyden
in session 1 2003.
Meeting Room and Times: Wednesdays, 3-6pm, QUAD G022.
Textbook:
Anil Nerode and Richard Shore, Logic for applications
References:
Ray Smullyan -- First-Order Logic, Dover Publications.
Topics Covered
The lectures follow the book closely, so there are generally no separate lecture notes.
- Lecture 1: Introduction, Basic Definitions of Propositional Resolution, Soundness
of the Resolution Rule.
- Lecture 2: Completeness of Propositional Resolution
Reading: Ch 1.1 -1.3, 1.8 pp. 49-55.
- Lecture 3: rest of completeness proof of
propositional resolution, Compactness, Infinite Trees, Konig's lemma.
Reading: as for lecture 2
- Lecture 4: completeness proof of propositional resolution without
assuming finiteness of S
Reading: Ch1, pp. 56-60.
- Lecture 5: Tableau proofs for propositional logic
Reading: Ch 1.4-1.5
- Lecture 6: Tableau proofs for propositional logic (ctd)
Reading: Ch 1.4-1.5
- Lecture 7: Completeness of Tableau proofs for propositional logic (ctd),
Introduction to Predicate Logic
Reading: Ch 1.4-1.5, Ch 2.1-2.4
- Lecture 8: Semantics of Predicate Logic, Intro to
tableaux proofs for predicate logic
Reading: Ch 4.4, 4.6
- Lecture 9:
tableaux proofs for predicate logic, and soundness
Reading: Ch 4.7
- Lecture 10:
tableaux proofs for predicate logic, completeness, Lowenheim-Skolem Theorem
Reading: Ch 4.7
- lecture 11: propositional Horn Clauses
- lecture 12: propositional Horn clauses ctd, Datalog
- lecture13: SLD resolution, unification
Lecture Notes
more notes
Assignments
Hand-written
will do. Please staple together the sheets, write your name, student
number and UNSW e-mail id at the top of the first page. All
assignments are due in the lecture the following week after they are
assigned, unless otherwise announced. Discussion of the broad approach to
a solution with your peers is permitted, All submissions should be
your own work. If you have collaborated with someone on solving a
problem, say so in your submission, and attribute percentages of
contribution for each. Grades will be divided accordingly. Penalties
for attempts to pass off joint work as your own may be as severe as a
mark of zero for the course.
Tutorial Thus 1-2, K17 L3 meeting room.
This page is maintained by the course instructor Ron van der Meyden