The Simple Deductive Data Retriever (SDDR) supports basic backward and forward chaining rules. The code was originally developed by Drew McDermott for the book Artificial Intelligence Programming by Eugene Charniak, Christopher Riesbeck, Drew McDermott and James Meehan. It's been extended and modified slightly for this class.

To understand what a deductive retriever does, see the deductive retrieval overview

Setting up the Deductive Retriever

SDDR is one of the local projects in CS325.

(ql:quickload "sddr")

This defines the package sddr where the retriever is defined, and sddr-tests where SDDR can be tested. To play with SDDR, do

(in-package :sddr-tests)

Using SDDR

The key function in SDDR is ask.

(ask query rules)

query is a clause. A query can have variables and functional terms. rules is a list of backward-chaining assertions assertions. Each assertion has the form

(<- consequent antecedent1 antecedent2 ...)

The consequent and antecedent are also clauses. They can have variables and functional terms.

ask calls prove which uses backward chaining and unification to find all possible ways the query can be proved, if any. ask will return a copy of query -- called an instantiation -- for each proof. Each proof is a list of bindings for the variables in the query and the rules used. ask replaces any variables in query with their bindings in the proof.

Negation in SDDR

SDDR implements "negation as failure". That means that (NOT clause) is true if clause can't be proven. For example, to define a general predicate (DIFFERENT x y) that is true if x and y are not equal:

(<- (same ?x ?x))

(<- (different ?x ?y) (not (same ?x ?y)))

Negation as failure is handy but has odd properties. You can't write a rule that asserts something is not true, i.e., used NOT in the consequent. NOT makes the logic non-monotonic. Mathematical logic is monotonic. That means if something was provable before you add a fact, it is still provable afterwards. Since adding a fact might make a proof based on NOT longer work, SDDR with NOT is non-monotonic.