From: Dragan Cvetkovic
Subject: Code for disjunctive normal form anyone?
Date: Tue, 09 Jun 1992 10:29:31 +0000
Message-ID: <1992Jun9.102931.17674@coli.uni-sb.de>

		Hi!
	Is there anyone who can send me LISP code for transforming formula
into disjunctive normal form, or at least point where can I find it. This
code is supposed to be a small part of my program, and I have no too much
time to do it myself.
			Thanks in advance
				Dragan, ······@coli.uni-sb.de

• Re: Code for disjunctive normal form anyone? Bruce Krulwich
  • Re: Code for disjunctive normal form anyone? Bruce Krulwich
• Re: Code for disjunctive normal form anyone? Raul Valdes-Perez

From: Bruce Krulwich
Subject: Re: Code for disjunctive normal form anyone?
Date: Tue, 09 Jun 1992 17:24:44 +0000
Message-ID: <KRULWICH.92Jun9112444@zowie.ils.nwu.edu>

······@coli.uni-sb.de (Dragan Cvetkovic) writes:

    	Is there anyone who can send me LISP code for transforming formula
    into disjunctive normal form, or at least point where can I find it. This
    code is supposed to be a small part of my program, and I have no too much
    time to do it myself.

Here's some code that may help.  It assumes a representation of formulas
(formulae?), called "items," as one of several different structure types for
propositions ("item-basic") conjunctions ("item-and"), disjunctions
("item-or"), universals, or existentials.  I'm sure that it can fairly easily
be converted to whatever representation you have.


(defun item-dnf (item)
  (cond ((item-basic-p item)
	 (make-item-or :item-list 
			(list (make-item-and :item-list (list item)))))
	((item-or-p item)
	 (make-item-or :item-list
			(apply #'append
				(mapcar #'(lambda (x)
					    (item-or-item-list (item-dnf x)))
					 (item-or-item-list item)))))
	((item-and-p item)
	 (let* ((cnf (item-cnf item))
		(list-of-cnf-lists (mapcar #'ITEM-OR-ITEM-LIST
					    (item-and-item-list cnf)))
		(cross-product (set-cross-product list-of-cnf-lists)))
	   (make-item-or :item-list
			  (mapcar #'(lambda (sym0.922)
				      (make-item-and :item-list sym0.922))
				   cross-product))))
	((item-not-p item) (item-negation (item-cnf (item-not-item item))))
	((item-univ-p item)
	 (make-item-univ :var (item-univ-var item)
			  :item (item-dnf (item-univ-item item))))
	(else (make-item-or :item-list
			     (list (make-item-and :item-list (list item)))))))



Bruce Krulwich
Institute for the Learning Sciences
········@ils.nwu.edu

 

From: Bruce Krulwich
Subject: Re: Code for disjunctive normal form anyone?
Date: Wed, 10 Jun 1992 17:57:14 +0000
Message-ID: <KRULWICH.92Jun10115714@zowie.ils.nwu.edu>

The DNF code I posted yesterday called a CNF function which I didn't include
in the message.  Here it is:

(defun item-cnf (item)
  (cond ((item-basic-p item)
	 (make-item-and :item-list
			 (list (make-item-or :item-list (list item)))))
	((item-or-p item)
	 (let* ((dnf (item-dnf item))
		(list-of-dnf-lists (mapcar #'ITEM-AND-ITEM-LIST
					    (item-or-item-list dnf)))
		(cross-product (set-cross-product list-of-dnf-lists)))
	   (make-item-and :item-list
			   (mapcar #'(lambda (sym0.920)
				       (make-item-or :item-list
						      sym0.920))
				    cross-product))))
	((item-and-p item)
	 (make-item-and :item-list
			 (apply #'APPEND
				 (mapcar #'(lambda (x)
					     (item-and-item-list (item-cnf x)))
					  (item-and-item-list item)))))
	((item-not-p item) (item-negation (item-dnf (item-not-item item))))
	((item-univ-p item)
	 (make-item-univ :var (item-univ-var item)
			  :item (item-cnf (item-univ-item item))))
	(else (make-item-and :item-list
			      (list (make-item-or :item-list (list item)))))))


 

From: Raul Valdes-Perez
Subject: Re: Code for disjunctive normal form anyone?
Date: Tue, 09 Jun 1992 20:58:50 +0000
Message-ID: <1992Jun09.205850.202911@cs.cmu.edu>

In article <·····················@coli.uni-sb.de>, ······@coli.uni-sb.de (Dragan Cvetkovic) writes:
|> 
|> 		Hi!
|> 	Is there anyone who can send me LISP code for transforming formula
|> into disjunctive normal form, or at least point where can I find it. This
|> code is supposed to be a small part of my program, and I have no too much
|> time to do it myself.
|> 			Thanks in advance
|> 				Dragan, ······@coli.uni-sb.de

I have some code for finding DNF or CNF that I wrote about 3 years ago
and am able to distribute.  I remember little about its internals, but 
in response to the above post I at least verified it to be 
not-obviously-broken.  It's written in CL and uses the Loop macro.

-- 
Raul E. Valdes-Perez		    ······@cs.cmu.edu
Carnegie Mellon University	    (412) 268-7127