;;; -*- Mode: LISP; Syntax: Common-lisp; Package: DTP; Base: 10 -*-
;;; This file was stolen from Matt Ginsberg's MVL 3/8/93
(in-package "DTP")
(defparameter *logical-operators* '(<= => <=> and or not))
(defun sentence-to-cnf (sentence)
"Rewrite constant predicates, then call CNF"
(when (find (car sentence) *logical-operators*)
(setq sentence
(cons (car sentence)
(mapcar #'rewrite-predicate (cdr sentence)) )))
(cnf sentence) )
(defun rewrite-predicate (predicate)
"P becomes (P), and (NOT Q) becomes (NOT (Q)), else unchanged"
(cond
((atom predicate)
(list predicate) )
((and (eq 'not (first predicate))
(atom (second predicate)) )
(list 'not (list (second predicate))) )
(t
predicate )))
(defun simplify-dnf (dnf)
(if (and (eq (car dnf) 'or)
(null (cddr dnf)) )
(second dnf)
dnf ))
;;;----------------------------------------------------------------------------
;; stuff to manipulate propositions
;; functions defined:
;;
;; cnf (p) returns conjunctive normal form
;; dnf (p) disjunctive normal form
;; standardize-operators removes => <= <=> if iff
;; negate (p) negates it
;; cnf-to-logic (cnf) inverts cnf
;; dnf-to-logic (dnf) inverts dnf
;; normal-form (p) returns something suitable for stating
;; conjunctive normal form. Remove the nonstandard operators from p and
;; then look at (car p):
;; 1. If it's NOT, then (cnf p) is the result of negating each term
;; inside (dnf (not (p))).
;; 2. If it's OR, then we have to combine the results of cnf'ing each
;; of the disjuncts. cnf-merge-lists does this, one disjunct at a
;; time.
;; 3. If it's AND, we just call the cnf'er and nconc the results
;; together.
;; 4. If it's none of these, it must be a term and we return ((p)).
(defun cnf (p)
(case (car (setq p (standardize-operators p)))
(not (napcar #'(lambda (l) (napcar #'negate l)) (dnf (second p))))
(or
(let (ans)
(dolist (item (cdr p) (nreverse ans))
(setq ans (cnf-merge-lists (cnf item) ans)))))
(and (mapcan #'cnf (cdr p)))
(otherwise (list (list p)))))
;; given a partial cnf expression d, and a new cnf exp c to be merged,
;; construct a list of all entries that have an entry from d followed by
;; one from c. As we go through, the list is maintained backwards, so
;; that we have terms with entries late in d early in the returned
;; answer. Three cases:
;; 1. If c is NIL, there is nothing to do. Return d.
;; 2. If d is NIL, there is still nothing to do, but we reverse c to
;; get d into "backwards" form.
;; 3. Otherwise, work through c and for each entry in it, work through
;; d, appending each entry of d onto that entry of c and pushing the
;; result onto the answer being accumulated. Note that this maintains
;; the "backwardness" of the answer. We make sure that each term in
;; the final answer is a fresh copy.
(defun cnf-merge-lists (c d)
(cond ((null c) d)
((null d) (nreverse c))
(t (let (ans)
(dolist (item c ans)
(push (append (car d) item) ans)
(dolist (x (cdr d)) (push (append x (copy-list item)) ans)))))))
;; remove nonstandard connectives from p. Handles =>, <=, <=>, if and
;; iff.
;; 1. (=> p1 ... pn q) means (if (and p1 ... pn) q), or
;; (or (not (and p1 ... pn)) q).
;; 2. (<= q p1 ... pn) means (if (and p1 ... pn) q) as well.
;; 3. (if p q) means (or (not p) q)
;; 4. (iff p q) means (or (and p q) (and (not p) (not q))); <=> is
;; similar.
(defun standardize-operators (p)
(case (car p)
(|=>| `(or (not (and . ,(butlast (cdr p)))) ,(car (last p))))
(|<=| `(or ,(second p) (not (and . ,(cddr p)))))
(if `(or ,(third p) (not ,(second p))))
((|<=>| iff) `(or (and ,(second p) ,(third p))
(and ,(negate (second p)) ,(negate (third p)))))
(otherwise p)))
;; dnf is a lot like cnf.
(defun dnf (p)
(case (car (setq p (standardize-operators p)))
(not (napcar #'(lambda (l) (napcar #'negate l)) (cnf (second p))))
(and
(let (ans)
(dolist (item (cdr p) (nreverse ans))
(setq ans (cnf-merge-lists (dnf item) ans)))))
(or (mapcan #'dnf (cdr p)))
(otherwise (list (list p)))))
;; negate a sentence. If it begins with not, return what's left.
;; Otherwise put a not on the front and return that.
(defun negate (p)
(if (eq 'not (car p)) (cadr p) (list 'not p)))
;; utility functions to turn a cnf expression, or a conjunct/disjunct,
;; into a logical sentence. They're all simple -- if the thing is a
;; list, push "and" or "or" on the front and proceed. Otherwise, just
;; return it.
(defun cnf-to-logic (cnf)
(conj-to-logic (mapcar #'disj-to-logic cnf)))
(defun dnf-to-logic (dnf)
(disj-to-logic (mapcar #'conj-to-logic dnf)))
(defun conj-to-logic (list)
(if (cdr list) (cons 'and list) (car list)))
(defun disj-to-logic (list)
(if (cdr list) (cons 'or list) (car list)))
;; *if-translation* controls how if is converted. If bc (the default),
;; two backward-chaining versions are created. If fc, two
;; forward-chaining versions. If mix, (if a b) translates to (<= b a)
;; and (=> a b).
(defparameter *if-translation* 'bc)
;; *equivalence-translation* controls how <=> is converted. If bc (the
;; default), two backward-chaining versions are created. If fc, two
;; forward-chaining versions. If mix, (<=> a b) translates to (<= a b)
;; and (=> a b).
(defparameter *equivalence-translation* 'bc)
;; normal form. Depends on (car p):
;; => invokes nf-forward
;; <= invokes nf-backward
;; if is treated by examining *if-translation*
;; <=>is treated by examining *equivalence-translation*
;; (or p1 ... pn) is turned into (<= p1 (not (and p2 ... pn)))
;; (iff a b) is (and (if a b) (if b a))
;; everything else is treated by calling the cnf'er and then calling
;; disj-to-logic on each term
(defun normal-form (p)
(case (car p)
(|=>| (nf-forward p))
(|<=| (nf-backward p))
(if
(case *if-translation*
(bc (nconc (nf-backward p)
(nf-backward `(if (not ,(third p)) (not ,(second p))))))
(fc (nconc (nf-forward p)
(nf-forward `(if (not ,(third p)) (not ,(second p))))))
(mix (nconc (nf-backward p) (nf-forward p)))))
(|<=>|
(case *equivalence-translation*
(bc (nconc (nf-backward (cons '|<=| (cdr p)))
(nf-backward (list '|<=| (third p) (second p)))))
(fc (nconc (nf-forward (cons '|=>| (cdr p)))
(nf-forward (list '|=>| (third p) (second p)))))
(mix (nconc (nf-backward (cons '|<=| (cdr p)))
(nf-forward (cons '|=>| (cdr p)))))))
(or (if (cddr p) (normal-form `(<= ,(second p) (not (and . ,(cddr p)))))
(normal-form (second p))))
(iff (nconc (normal-form (cons 'if (cdr p)))
(normal-form (list 'if (third p) (second p)))))
(and (mapcan #'normal-form (cdr p)))
(otherwise (napcar #'disj-to-logic (cnf p)))))
;; normal form for forward-chaining. Convert to cnf, then for each
;; term (or p1 ... pn), rewrite it as p1 (if n=1) or
;; (=> (not p1) ... (not pn-1) pn)
(defun nf-forward (p)
(napcar #'(lambda (x)
(if (cdr x)
`(=> ,.(napcar #'negate (butlast x)) ,(car (last x)))
(car x)))
(cnf p)))
;; backward-chaining. Convert to cnf, then for each term (or p1 ... pn),
;; rewrite it as p1 (if n=1) or (<= p1 (not p2) ... (not pn))
(defun nf-backward (p)
(napcar #'(lambda (x)
(if (cdr x)
`(<= ,(car x) . ,(napcar #'negate (cdr x)))
(car x)))
(cnf p)))