;;;;;;;;;
;; III ;;
;;;;;;;;;
;; subset
;;
;; Checks if every element of a is a member of b.
(defun subset (a b)
(cond ((null a) t)
((not (member (car a) b :test #'set-equal)) nil)
(t (subset (cdr a) b))))
;; set-equal
;;
;; Checks if a is a subset of b and b is a subset of a (which implies
;; set equality).
(defun set-equal (a b)
(if (or (atom a) (atom b)) (equal a b)
(and (subset a b) (subset b a))))
;; pl-resolution-helper
;;
;; This function preforms the bulk of the resolution algorithm. It
;; starts by finding salient clashes between pairs of previously
;; observed clauses and newly generated clauses (clashes are salient
;; if they result in exactly one new clause; otherwise, either there
;; is no clash or all resulting clauses have conjugate literal pairs).
;; Next, it checks to see if any clashes resulted in box, terminating
;; with nil (unsatisfiable) if so, and otherwise checks whether any
;; new clauses were introduced, terminating with t (satisfiable) if
;; not. Finally, pl-resolution recurses, adding clauses generated
;; this step to the list of observed clauses.
;;
;; This is not the fastest implementation of recursion, but it is not
;; the worst. We save time by not considering clashes between the
;; same two clauses more than once, but we potentially waste time by
;; checking for clashes between previously observed clauses and new
;; clauses that immediately resulted from them, as well as between
;; new clauses and themselves.
(defun pl-resolution-helper (cs rs)
;; obtain list of new clash results
(let ((next (delete-duplicates
(loop
for c in cs
append (loop
for r in rs
append (let ((res (clash c r)))
;; keep if clashes exactly once;
;; results meaningless otherwise
(if (= (length res) 1) res nil))))
;; clauses are sets; find dups ignoring order of terms
:test #'set-equal)))
;; if box or nothing new, we're done
(cond ((member nil next) nil)
((subset next cs) t)
;; otherwise, keep checking with new clauses
(t (pl-resolution-helper (union next cs :test #'set-equal)
next)))))
;; pl-resoultion
;;
;; A simple wrapper for the above. Note that this function expects a
;; list of claueses for input, not a sentence. You should call
;; cnf-list on sentences before calling pl-resolution.
(defun pl-resolution (cs)
;; check for box on the off chance that we start with it
(if (member nil cs) nil
;; otherwise proceed with normal resolution
(pl-resolution-helper cs cs)))
;;;;;;;;
;; IV ;;
;;;;;;;;
;; and-or-not
;;
;; Converts a sentence in PL or FOL such that it only uses logical
;; opperators _and, _or, and _not.
(defun and-or-not (s)
(cond ((atom s) s)
((equal (car s) '_implies)
(let ((a (and-or-not (cadr s)))
(b (and-or-not (caddr s))))
`(_or (_not ,a) ,b)))
((equal (car s) '_iff)
(let ((a (and-or-not (cadr s)))
(b (and-or-not (caddr s))))
`(_or (_and ,a ,b) (_and (_not ,a) (_not ,b)))))
(t (cons (car s) (mapcar #'and-or-not (cdr s))))))
;; deep-not
;;
;; Pushes _not's as deep as possible, eliminating double negatives.
(defun deep-not (s)
(cond ((atom s) s)
((equal (car s) '_not)
(cond ((equal (cadr s) nil) t)
((equal (cadr s) t) nil)
((atom (cadr s)) s)
((equal (caadr s) '_and)
(list '_or (deep-not (list '_not (cadadr s)))
(deep-not (list '_not (car (cddadr s))))))
((equal (caadr s) '_or)
(list '_and (deep-not (list '_not (cadadr s)))
(deep-not (list '_not (car (cddadr s))))))
((equal (caadr s) '_not) (deep-not (cadadr s)))
(t s)))
(t (cons (car s) (mapcar #'deep-not (cdr s))))))
;; or-list
;;
;; Converts a disjunction into a list of its components.
(defun or-list (s)
(cond ((atom s) (list s))
((equal (car s) '_not) (list s))
((equal (car s) '_or) (union (or-list (cadr s))
(or-list (caddr s))
:test #'equal))
(t (list s))))
;; definite-list-helper
;;
;; This function separates a simple disjunction list into lists for
;; positive and negative terms.
(defun definite-list-helper (c &optional neg pos)
(cond ((null c) (list neg pos))
;; c should not contain atoms in our FOL syntax, but handle
;; them appropriately if we find any; an example is nil
((atom (car c)) (definite-list-helper (cdr c) neg (cons (car c) pos)))
;; terms that start with _not go into the list of negatives
((equal (caar c) '_not)
(definite-list-helper (cdr c) (cons (cadar c) neg) pos))
;; everything else is possitive
(t (definite-list-helper (cdr c) neg (cons (car c) pos)))))
;; definte-list
;;
;; Calls the above after processing the sentence into a disjunction
;; list. Afterwards, performs a simple sanity check. Note that this
;; sanity check is not thorough; you should look at this function's
;; results for your input to make sure there are no strange
;; constructs.
(defun definite-list (s)
(let ((res (definite-list-helper (or-list (deep-not (and-or-not s))))))
(if (> (length (cadr res)) 1) (error "~s is not first-order definite" s)
res)))
;; subst-list
;;
;; Apply a variable substitution to a sentence in FOL.
(defun subst-list (tree pairs)
(reduce (lambda (a b) (subst (cadr b) (car b) a)) (cons tree pairs)))
;; next-apart
;;
;; Global variable used by standardize-apart to generate new symbols.
(defparameter next-apart 0)
;; standardize-apart-helper
;;
;; Does the work of finding variables and suggesting new symbols.
;; Note that multiple symbols are generated for the same variable if
;; the variable occurs more than once, so the calling function should
;; be sure to remove duplicates before applying the substitution.
(defun standardize-apart-helper (p)
(cond ((equal p nil) nil)
((equal p t) nil)
;; atoms other than t and nil are variables
((atom p) (list (list p (incf next-apart))))
;; don't standardize consts
((equal (car p) '_const) nil)
;; recurse otherwise
(t (mapcan #'standardize-apart-helper (cdr p)))))
;; standardize-apart
;;
;; Replace existing variables with new symbols to ensure we never have
;; problems with shared variables in unification.
(defun standardize-apart (p)
;; the helper only suggests replacements; here we apply them, after
;; removing any duplicate suggestings (not actually necessary with
;; subst-list, but a good percaution)
(subst-list p (delete-duplicates
(standardize-apart-helper p)
:test (lambda (a b) (equal (car a) (car b))))))
;; p-rename
;;
;; Check if two proven terms differ only by variable names. We
;; accomplish this by attempting to unify the two terms. If variables
;; are only mapped to other variables, and no variable occurs in the
;; map more than once (which would imply that constraint on matching
;; components differs between the terms), then a renaming has been
;; found.
(defun p-rename (a b)
(let ((pairs (unify a b)))
;; failures to unify are of course not renamings
(and (not (equal pairs 'failure))
;; if we substitute with any constants, not renaming
(not (loop
for pair in pairs
when (not (atom (cadr pair)))
return t))
;; if variable occurs twice, not renaming (see description)
(let ((vars (apply #'nconc pairs)))
(equal vars (remove-duplicates vars))))))
;; d-rename
;;
;; Check if a definite clause is a renaming of another definite
;; clause. This is an exceedingly hard problem, as terms in clauses
;; may have different sort orders, and and variables shared between
;; terms must be recognized. Fortunately, just deeming all clauses to
;; not rename each other causes no problems with my implementation of
;; the algorithm, because each added clause is one term shorter than
;; its ancestors, and no clause is ever unified with with the same
;; proven term.
;;
;; Note that this function is not acutally used; I removed calls to it
;; because it was just making things complicated, and never quite
;; worked.
(defun d-rename (a b) nil)
;; learn
;;
;; Finds all ways in which a proven term can be unified with portions
;; of a definite clause. New clauses are formed by removing unified
;; terms. Note that only one unified term is removed at a time, so
;; new clauses should be checked again with the same proven term to
;; see if there are more possible unifications.
(defun learn (d p)
(loop
for terms on (car d)
append (let ((pairs (unify p (car terms))))
;; ignore failure (they prove nothing)
(if (equal pairs 'failure) nil
;; otherwise, prepare results for collection
(list (subst-list (cons (append prev (cdr terms)) (cdr d))
pairs))))
collect (car terms) into prev))
;; solve
;;
;; Checks if any newly proven terms unify with queries.
(defun solve (qs ps)
(loop
for q in qs
append (loop
for p in ps
append (let ((pairs (unify q p)))
;; ignore failures (they prove nothing)
(if (equal pairs 'failure) nil
;; otherwise, prepare results for collection
(list (subst-list q pairs)))))))
;; fol-fc-ask-helper
;;
;; Does the bulk of the work for forward-chaining. I've implemented a
;; slightly different algorithm than illustrated on page 282 of
;; Russell/Norvig. The book discribes a BFS algorithm that seeks a
;; single answer for a single query, but the following is an
;; exhaustive DFS-style search that can find many answers for each of
;; many queries. Also, the process of finding unifying terms with
;; unsatisfied clauses is somewhat simplified (the book actually omits
;; any discussion on how this should be done) and more closely
;; resembles resolution than traditional forward-chaining: new clauses
;; are formed by "clashing" known terms against existing clauses'
;; preconditions.
;;
;; The exhaustive nature of this algorithm worsens its exponential
;; time requirements, but its wanton creation of new clauses actually
;; helps reduce repeated work at the expense of memory. There are
;; better ways to implement forward-chaining, but for the purposes of
;; this assignment, they are not worthwhile. Note that this algorithm
;; does speed itself up significantly by only checking for
;; satisfaction of preconditions with newly proven terms.
(defun fol-fc-ask-helper (ds kb ps learned qs solved)
;; we're finished if we ever run out of newly proven terms
(cond ((null ps) solved)
;; on the other hand, if we run out of definite clauses, start
;; over with the next proven term
((null ds) (fol-fc-ask-helper kb kb (cdr ps) learned qs solved))
;; otherwise, proceed to check for new deductions
(t (let* ((cur-p (standardize-apart (car ps)))
;; find what we can learn
(next (learn (car ds) cur-p))
;; separate this into new partially satisfied
;; definite clauses...
(next-ds (loop
for d in next
when (car d)
collect d))
;; ...and into newly proven terms
(next-ps (loop
for d in next
when (and (null (car d))
(not (member
(standardize-apart (caadr d))
learned :test #'p-rename)))
collect (caadr d)))
;; finally, check if we've answered any queries
(res (solve qs next-ps)))
;; and recurse
(fol-fc-ask-helper (append next-ds (cdr ds))
(append next-ds kb)
(cons (car ps) (append next-ps (cdr ps)))
(append next-ps learned)
qs (append res solved))))))
;; fol-fc-ask
;;
;; Searches for answers for a list of queries, qs, within a
;; knowledge-base, kb, by means of forward-chaining. If more than one
;; answer exists for a particular query, fol-fc-ask returns all of
;; them (in no particular arrangement). kb must be a list of FOL
;; definite clauses in list format, and qs must be a list of FOL
;; terms:
;;
;; kb: ((((LivesIn x r) (LivesIn y r)) ((Roommate x y)))
;; (((LivesIn x r) (Roommate x y)) ((LivesIn y r)))
;; (((LivesIn y r) (Roommate x y)) ((LivesIn x r)))
;; (((Roommate x y)) ((Roomate y x)))
;; (() ((LivesIn (_const Bill) (_const Room201))))
;; (() ((Roommate (_const Ted) (_const Bill))))
;; (() ((LivesIn (_const Steve) (_const Room201)))))
;;
;; qs: ((LivesIn (_const Ted) r)
;; (Roommate (_const Bill) x))
;;
;; Note that sentences in FOL representing definite clauses can be
;; converted into list format through the use of the definite-list
;; function.
(defun fol-fc-ask (kb qs)
;; separate the kb into partially satisfied definte clauses...
(let* ((init-kb (loop
for d in kb
when (car d)
collect d))
;; ...and into terms handed to us as true
(init-learned (loop
for d in kb
when (and (null (car d))
(not (member
(standardize-apart (caadr d))
res :test #'p-rename)))
collect (caadr d) into res
finally (return res)))
;; standardize apart the queries just once in the beginning;
;; this is okay because bits of queries have no chance of
;; being substituted into the knowledge base
(standard-qs (mapcar #'standardize-apart qs))
;; find any answers to queries we have from the beginning
(init-solved (solve standard-qs init-learned)))
;; and begin
(fol-fc-ask-helper init-kb init-kb
init-learned init-learned
standard-qs init-solved)))