share/logic/logic.lisp

   1 #|
   2 ; logic.mac--Logic algebra package for Maxima CAS.
   3 ; Copyright (c) 2008--2009 Alexey Beshenov <al@beshenov.ru>.
   4 ;
   5 ; Version 2.11. Last modified 2009-01-07.
   6 ;
   7 ; logic.mac is free software; you can redistribute it and/or modify it
   8 ; under the terms of the GNU Lesser General Public License as published
   9 ; by the Free Software Foundation; either version 2.1 of the License,
  10 ; or (at your option) any later version.
  11 ;
  12 ; logic.mac is distributed in the hope that it will be useful, but
  13 ; WITHOUT ANY WARRANTY; without even the implied warranty of
  14 ; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
  15 ; General Public License for more details.
  16 ;
  17 ; You should have received a copy of the GNU General Public License
  18 ; along with the logic.mac; see the file COPYING. If not, write to the
  19 ; Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
  20 ; Boston, MA 02110-1301, USA.
  21 |#
  22
  23
  24 (defvar $logic_mac_version 2.11)
  25
  26 (defvar use-maxima-logic-operators t)
  27
  28 (if use-maxima-logic-operators
  29   (progn
  30     (defvar *not-op* 'mnot)
  31     ($texput "not" " \\neg " '$prefix)
  32     (defvar *and-op* 'mand)
  33     ($texput "and" " \\wedge " '$nary)
  34     (defvar *or-op* 'mor)
  35     ($texput "or" " \\vee " '$nary))
  36   (progn
  37     ($prefix "log-not" 70)
  38     (defvar *not-op* '$log-not)
  39     ($texput "log-not" " \\neg " '$prefix)
  40     ($nary "log-and" 65)
  41     (defvar *and-op* '$log-and)
  42     ($texput "log-and" " \\wedge " '$nary)
  43     ($nary "log-or" 60)
  44     (defvar *or-op* '$log-or)
  45     ($texput "log-or" " \\vee " '$nary)))
  46
  47 ($nary "nand" 62)
  48 (defvar *nand-op* '$nand)
  49 ($texput "nand" " \\mid " '$nary)
  50
  51 ($nary "nor" 61)
  52 (defvar *nor-op* '$nor)
  53 ($texput "nor" " \\downarrow " '$nary)
  54
  55 ($infix "implies" 59)
  56 (defvar *implies-op* '$implies)
  57 ($texput "implies" " \\rightarrow " '$infix)
  58
  59 ($nary "eq" 58)
  60 (defvar *eq-op* '$eq)
  61 ($texput "eq" " \\sim " '$nary)
  62
  63 ($nary "xor" 58)
  64 (defvar *xor-op* '$xor)
  65 ($texput "xor" " \\oplus " '$nary)
  66
  67 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  68
  69 (defun get-maxima-operator (expr)
  70   (if (and (listp expr) expr (listp (car expr)) (car expr))
  71     (caar expr)
  72     nil))
  73
  74 (defun contains-operator (expr op)
  75   (let
  76     ((o (get-maxima-operator expr)) args)
  77     (setf args (if o (cdr expr) nil))
  78     (if
  79       (eq o op)
  80       t
  81       (member t (mapcar #'(lambda (e) (contains-operator e op)) args)))))
  82
  83 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  84
  85 (defun replicate (n e)
  86   (if (and (integerp n) (>= n 0))
  87     (if (= n 0) nil (cons e (replicate (1- n) e)))
  88     (error "Invalid arguments to 'replicate'")))
  89
  90 (defun zip (l1 l2)
  91   (if (or (not (listp l1)) (not (listp l2)) (/= (length l1) (length l2)))
  92     (error "Invalid arguments to 'zip'"))
  93   (if (null l1)
  94     l1
  95     (cons (cons (car l1) (car l2)) (zip (cdr l1) (cdr l2)))))
  96
  97 (defun remove-nth (n l)
  98   (cond
  99     ((or (not (integerp n)) (< n 0)) (error "Invalid argumet to 'remove-nth'"))
 100     ((= n 0) (cdr l))
 101     (t (cons (car l) (remove-nth (1- n) (cdr l))))))
 102
 103 (defun multiset-to-hash (l)
 104   (mapcar
 105     #'(lambda (e) (list e (count e l :test 'equal)))
 106     (remove-duplicates l :test 'equal)))
 107
 108 (defun hash-to-multiset (h)
 109   (mapcan (lambda (he) (replicate (second he) (first he))) h))
 110
 111 (defun cancel-pairs-in-hash (h)
 112   (mapcar (lambda (he) (list (first he) (mod (second he) 2))) h))
 113
 114 (defun cancel-pairs (l)
 115   (hash-to-multiset (cancel-pairs-in-hash (multiset-to-hash l))))
 116
 117 (defun subst-recursive (expr pairs)
 118   (if pairs
 119     (let ((p (car pairs)))
 120       (subst (cdr p) (car p) (subst-recursive expr (cdr pairs))))
 121     expr))
 122
 123 (defun disjoin-list (pred lst)
 124   (if (null lst)
 125     '(nil nil)
 126     (let ((dl (disjoin-list pred (cdr lst))))
 127       (if (funcall pred (car lst))
 128         (list (cons (car lst) (first dl)) (second dl))
 129         (list (first dl) (cons (car lst) (second dl)))))))
 130
 131 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 132
 133 ; t or nil
 134 (defun booleanp (x)
 135   (or (eq x t) (eq x nil)))
 136
 137 (defun logic-sort-comparator (x y)
 138   (cond
 139     ((and (not (booleanp x)) (booleanp y)) t)
 140     ((and (booleanp x) (not (booleanp y))) nil)
 141     ((and (not (listp x)) (listp y)) nil)
 142     ((and (listp x) (not (listp y))) t)
 143     ((and (listp x) (listp y) (< (length x) (length y))) nil)
 144     ((and (listp x) (listp y) (> (length x) (length y))) t)
 145     (t ($orderlessp x y))))
 146
 147 (defun sort-symbols (seq)
 148   (sort seq 'logic-sort-comparator))
 149
 150 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 151
 152 ; op (x_1, ..., f(y_1, ..., y_m), ..., x_n) =>
 153 ;                                         op (x_1, ..., y_1, ..., y_m, ..., x_n)
 154 (defun flatten-nested (args op)
 155   (let
 156     ((nested-exprs nil)
 157      (other nil))
 158     (loop while args do
 159       (if
 160         (eq (get-maxima-operator (car args)) op)
 161         (setq nested-exprs (cons (car args) nested-exprs))
 162         (setq other (cons (car args) other)))
 163       (setq args (cdr args)))
 164     (setq
 165       nested-exprs
 166       (mapcar #'(lambda (e) (flatten-nested (cdr e) op)) nested-exprs))
 167     (if nested-exprs
 168       (append other (apply 'append nested-exprs))
 169       other)))
 170
 171 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 172
 173 ; Logic functions
 174
 175 ; Implication
 176 (defun simp-implies (x y)
 177   (cond
 178     ((eq x nil) t)
 179     ((and (eq x t) (eq y t)) t)
 180     ((and (eq x t) (eq y nil)) nil)
 181     (t (list (list *implies-op* 'simp) x y))))
 182
 183 ; Webb-operation or Peirce arrow (Quine's dagger, NOR)
 184 (defun simp-nor (&rest args)
 185   (if
 186     (member t args)
 187     (return-from simp-nor nil))
 188   (setf args (remove-duplicates (remove nil args) :test 'equal))
 189   (cond
 190     ((null args) t)
 191     ((eql (length args) 1) (simp-not (car args)))
 192     (t (cons (list *nor-op* 'simp) (sort-symbols args)))))
 193
 194 ; Sheffer stroke (alternative denial, NAND)
 195 (defun simp-nand (&rest args)
 196   (if
 197     (member nil args)
 198     (return-from simp-nand t))
 199   (setf args (remove-duplicates (remove t args) :test 'equal))
 200   (cond
 201     ((null args) nil)
 202     ((eql (length args) 1) (simp-not (car args)))
 203     (t (cons (list *nand-op* 'simp) (sort-symbols args)))))
 204
 205 ; Equivalence
 206 (defun simp-eq (&rest args)
 207   (setf args (cancel-pairs (remove t (flatten-nested args *eq-op*))))
 208   (cond
 209     ((null args) t)
 210     ((eql (length args) 1) (car args))
 211     (t (cons (list *eq-op* 'simp) (sort-symbols args)))))
 212
 213 ; Sum modulo 2 (exclusive or)
 214 (defun simp-xor (&rest args)
 215   (setf args (cancel-pairs (remove nil (flatten-nested args *xor-op*))))
 216   (cond
 217     ((null args) nil)
 218     ((eql (length args) 1) (car args))
 219     (t (cons (list *xor-op* 'simp) (sort-symbols args)))))
 220
 221 ; returns t if args = (... x ... not x ...)
 222 ; used in simp-and and simp-or
 223 (defun x-not-x (args)
 224   (let
 225     ((neg
 226        (disjoin-list
 227          #'(lambda (e) (eq (get-maxima-operator e) *not-op*)) args)))
 228     (not
 229       (null
 230         (intersection
 231           (mapcar 'cadr (first neg)) (second neg) :test 'equal)))))
 232
 233 ; Logical AND (conjunction)
 234 (defun simp-and (&rest args)
 235   (setf args (flatten-nested args *and-op*))
 236   (if
 237     (member nil args)
 238     (return-from simp-and nil))
 239   (setf args (remove-duplicates (remove t args) :test 'equal))
 240   (cond
 241     ((null args) t)
 242     ((eql (length args) 1) (car args))
 243     (t
 244       (if (x-not-x args)
 245         nil
 246         (cons (list *and-op* 'simp) (sort-symbols args))))))
 247
 248 ; Logical OR (disjunction)
 249 (defun simp-or (&rest args)
 250   (setf args (flatten-nested args *or-op*))
 251   (if
 252     (member t args)
 253     (return-from simp-or t))
 254   (setf args (remove-duplicates (remove nil args) :test 'equal))
 255   (cond
 256     ((null args) nil)
 257     ((eql (length args) 1) (car args))
 258     (t
 259       (if (x-not-x args)
 260         t
 261         (cons (list *or-op* 'simp) (sort-symbols args))))))
 262
 263 ; Logical NOT (negation)
 264 (defun simp-not (x)
 265   (cond
 266     ((eq (get-maxima-operator x) *not-op*) (cadr x))
 267     ((eq x nil) t)
 268     ((eq x t) nil)
 269     (t (list (list *not-op* 'simp) x))))
 270
 271 (defun apply-op (op args)
 272   (cond
 273     ((eq op *and-op*) (apply 'simp-and args))
 274     ((eq op *xor-op*) (apply 'simp-xor args))
 275     ((eq op *not-op*) (apply 'simp-not args))
 276     ((eq op *or-op*) (apply 'simp-or args))
 277     ((eq op *nor-op*) (apply 'simp-nor args))
 278     ((eq op *nand-op*) (apply 'simp-nand args))
 279     ((eq op *eq-op*) (apply 'simp-eq args))
 280     ((eq op *implies-op*) (apply 'simp-implies args))
 281     (t (cons (list op) args))))
 282
 283 (defun logic-simp (expr)
 284   (let
 285     ((op (get-maxima-operator expr)) args)
 286     (setf args (if op (mapcar 'logic-simp (cdr expr)) nil))
 287     (if op
 288       (apply-op op args)
 289       expr)))
 290
 291 (defun $logic_simp (expr) (logic-simp expr))
 292
 293 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 294
 295 #|
 296 ;
 297 ; (all-charfuns 1) => ((nil) (t))
 298 ;
 299 ; (all-charfuns 2) => ((nil nil) (nil t) (t nil) (t t))
 300 ;
 301 ; (all-charfuns 3) => ((nil nil nil) (nil nil t) (nil t nil) (nil t t)
 302 ;                      (t nil nil) (t nil t) (t t nil) (t t t))
 303 ;
 304 ; ...
 305 ;
 306 |#
 307
 308 (defun all-charfuns (n)
 309   (if (not (and (integerp n) (>= n 1)))
 310     (error "Invalid argument to 'all-charfuns'"))
 311   (cond
 312     ((= n 1) '((nil) (t)))
 313     (t
 314       (let
 315         ((pre (all-charfuns (1- n))))
 316         (append
 317           (mapcar (lambda (l) (cons nil l)) pre)
 318           (mapcar (lambda (l) (cons t l)) pre))))))
 319
 320 ; List of values for all-charfuns, 2^n elements
 321 (defun characteristic-vector (expr &rest args)
 322   (if (null args)
 323     (setf args (list-of-variables expr)))
 324   (if (null args)
 325     (list expr)
 326     (let (vals (n (length args)))
 327       (setf vals (mapcar #'(lambda (l) (zip args l)) (all-charfuns n)))
 328       (mapcar #'(lambda (v) (logic-simp (subst-recursive expr v))) vals))))
 329
 330 (defun list-of-variables (expr)
 331   (sort-symbols (cdr ($listofvars expr))))
 332
 333 (defun $characteristic_vector (expr &rest args)
 334   (cons '(mlist simp) (apply 'characteristic-vector (cons expr args))))
 335
 336 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 337
 338 ; Conversion to the Zhegalkin basis {and, xor}
 339 (defun zhegalkin-basis-substitute (expr)
 340   (let
 341     ((op (get-maxima-operator expr)) args)
 342     (setf args (if op (mapcar 'zhegalkin-basis-substitute (cdr expr)) nil))
 343     (cond
 344       ; not x => x xor t
 345       ((eq op *not-op*) (simp-xor (car args) t))
 346       ; x implies y => (x and y) xor x xor t
 347       ((eq op *implies-op*)
 348         (simp-xor (apply 'simp-and args) (first args) t))
 349       ; x1 nand x2 nand x3 ... nand xn => (x1 and x2 and x3 ... and xn) xor t
 350       ((eq op *nand-op*) (simp-xor (apply 'simp-and args) t))
 351       ; x nor y => (x or y) xor t
 352       ((eq op *nor-op*)
 353         (simp-xor
 354           (zhegalkin-basis-substitute (simp-or (first args) (second args)))
 355           t))
 356       ; x or y => (x and y) xor x xor y
 357       ((eq op *or-op*)
 358         (let (zhegform)
 359           (setf zhegform
 360             (simp-xor
 361               (simp-and (first args) (second args))
 362               (first args) (second args)))
 363           (setf args (cddr args))
 364           (loop while args do
 365             (setf zhegform
 366               (simp-xor
 367                 (simp-and zhegform (car args))
 368                 zhegform
 369                 (car args)))
 370             (setf args (cdr args)))
 371           zhegform))
 372       ; a eq b => a xor b xor t
 373       ; a eq b eq c => a xor b xor c
 374       ; a eq b eq c eq d => a xor b xor c xor d xor t
 375       ; a eq b eq c eq d eq e => a xor b xor c xor d xor e
 376       ; ...
 377       ((eq op *eq-op*)
 378         (apply 'simp-xor
 379           (if (evenp (length args)) (cons t args) args)))
 380       (op (apply-op op args))
 381       (t expr))))
 382
 383 ; acts like Maxima "expand" on ordinary polynomial ring,
 384 ; but on Zhegalkin polynomials
 385 (defun zhegalkin-basis-expand (expr)
 386   (let
 387     ((op (get-maxima-operator expr)) args)
 388     (setf args (if op (mapcar 'zhegalkin-basis-expand (cdr expr)) nil))
 389     (cond
 390       ((eq op *and-op*)
 391         (let
 392           ((xor-expression
 393              (find-if
 394                (lambda (e) (eq (get-maxima-operator e) *xor-op*))
 395                (cdr expr))))
 396           (if xor-expression
 397             (let
 398               ((xor-args (cdr xor-expression))
 399                (and-args
 400                  (remove xor-expression (cdr expr) :test 'equal)))
 401               (zhegalkin-basis-expand
 402                 (apply 'simp-xor
 403                   (mapcar
 404                     (lambda (e) (apply 'simp-and (cons e and-args)))
 405                     xor-args))))
 406             expr)))
 407       ((eq op *xor-op*) (apply 'simp-xor args))
 408       (t expr))))
 409
 410 (defun $zhegalkin_form (expr)
 411   (zhegalkin-basis-expand (zhegalkin-basis-substitute expr)))
 412
 413 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 414
 415 (defun $logic_equiv (expr1 expr2)
 416   (equal
 417     ($zhegalkin_form expr1)
 418     ($zhegalkin_form expr2)))
 419
 420 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 421
 422 (defun subst-not (expr)
 423   (let
 424     ((op (get-maxima-operator expr)))
 425     (if op
 426       (cons (list op) (mapcar 'subst-not (cdr expr)))
 427       (simp-not expr))))
 428
 429 ; f^* (x_1, ..., x_n) = not f (not x_1, ..., not x_n)
 430 (defun $dual_function (expr)
 431   (logic-simp (simp-not (subst-not expr))))
 432
 433 ; f = f^*
 434 (defun $self_dual (expr)
 435   ($logic_equiv expr ($dual_function expr)))
 436
 437 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 438
 439 (defun closed-under (expr x)
 440   (let
 441     (val n (args (list-of-variables expr)))
 442     (setf n (length args))
 443     (setf val (zip args (replicate n x)))
 444     (eq (logic-simp (subst-recursive expr val)) x)))
 445
 446 ; f (nil, ..., nil) = nil
 447 (defun $closed_under_f (expr)
 448   (closed-under expr nil))
 449
 450 ; f (t, ..., t) = t
 451 (defun $closed_under_t (expr)
 452   (closed-under expr t))
 453
 454 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 455
 456 (defun $monotonic (expr &rest args)
 457   (let
 458     (prev-value (charvec (apply 'characteristic-vector (cons expr args))))
 459     (if charvec
 460       (progn
 461         (setf prev-value (car charvec))
 462         (setf charvec (cdr charvec))
 463         (loop while charvec do
 464           (if
 465             (and
 466               (eq (car charvec) nil)
 467               (eq prev-value t))
 468             (return-from $monotonic nil))
 469           (setf prev-value (car charvec))
 470           (setf charvec (cdr charvec)))
 471         t)
 472       t)))
 473
 474 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 475
 476 (defun $linear (expr)
 477   (not (contains-operator ($zhegalkin_form expr) *and-op*)))
 478
 479 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 480
 481 ; Post's theorem
 482
 483 (defun post-table (&rest expressions)
 484   (mapcar
 485     (lambda (fn) (mapcar fn expressions))
 486     '($self_dual $closed_under_f $closed_under_t $linear $monotonic)))
 487
 488 (defun functionally-complete (table)
 489   (if
 490     (null table)
 491     (return-from functionally-complete nil))
 492   (loop while table do
 493     (if
 494       (not (member nil (car table)))
 495       (return-from functionally-complete nil))
 496     (setf table (cdr table)))
 497   t)
 498
 499 (defun $functionally_complete (&rest expressions)
 500   (functionally-complete (apply 'post-table expressions)))
 501
 502 ; Basis is a complete system without redundant functions
 503 (defun $logic_basis (&rest expressions)
 504   (let
 505     ((table (apply 'post-table expressions))
 506      (n (length expressions)))
 507     (if (functionally-complete table)
 508       (if (= n 1)
 509         (return-from $logic_basis t))
 510       (return-from $logic_basis nil))
 511     (loop for i from 0 to (1- n) do
 512       (if
 513         (functionally-complete
 514           (mapcar (lambda (e) (remove-nth i e)) table))
 515         (return-from $logic_basis nil)))
 516     t))
 517
 518 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 519
 520 ;; Logic differentiation
 521
 522 #|
 523 ;
 524 ;                               dy
 525 ;   (1)                        --- = false
 526 ;                              dx
 527 ;
 528 ; where y is a variable which not depends on x.
 529 ;
 530 ;
 531 ;                               dx
 532 ;   (2)                        --- = true
 533 ;                              dx
 534 ;
 535 ;
 536 ;              d
 537 ;   (3)       --- [x  and ... and x ] = x  and x  ... and x
 538 ;             dx    1              n     2      3          n
 539 ;               1
 540 ;
 541 ;
 542 ;                     d             df     dg
 543 ;   (4)              -- [g xor f] = -- xor --
 544 ;                    dx             dx     dx
 545 ;
 546 ;
 547 ; TODO: higher orders / mixed
 548 ;
 549 |#
 550
 551 (defun diff-zhegalkin-form (expr x)
 552   (let ((op (get-maxima-operator expr)))
 553     (cond
 554       ((null op) (eq expr x))
 555       ((eq op *xor-op*)
 556         (apply
 557           'simp-xor
 558           (mapcar #'(lambda (e) (diff-zhegalkin-form e x)) (cdr expr))))
 559       ((eq op *and-op*)
 560         (let ((args (cdr expr)))
 561           (if (member x args) (apply 'simp-and (remove x args)) nil)))
 562       (t (error "Not a Zhegalkin form in diff-zhegalkin-form: '~s'" expr)))))
 563
 564 (defun $logic_diff (expr x)
 565   (diff-zhegalkin-form ($zhegalkin_form expr) x))
 566
 567 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 568
 569 ; Coversion to the Boolean basis {and, or, not}
 570 (defun boolean-basis-substitute (expr)
 571   (let
 572     ((op (get-maxima-operator expr)) args)
 573     (setf args (if op (mapcar 'boolean-basis-substitute (cdr expr)) nil))
 574     (cond
 575       ; x implies y => (not x) or y
 576       ((eq op *implies-op*) (simp-or (simp-not (first args)) (second args)))
 577       ; x1 nand ... nand xn => not (x1 and ... and xn)
 578       ((eq op *nand-op*) (simp-not (apply 'simp-and args)))
 579       ; x1 nor ... not xn => not (x1 or ... or xn)
 580       ((eq op *nor-op*) (simp-not (apply 'simp-or args)))
 581       ; x eq b => ((not x) or y) and ((not y) or x)
 582       ((eq op *eq-op*)
 583         (let (boolform)
 584           (setf boolform
 585             (simp-and
 586               (simp-or (simp-not (first args)) (second args))
 587               (simp-or (simp-not (second args)) (first args))))
 588           (setf args (cddr args))
 589           (loop while args do
 590             (setf boolform
 591               (simp-and
 592                 (simp-or (simp-not boolform) (car args))
 593                 (simp-or (simp-not (car args)) boolform)))
 594             (setf args (cdr args)))
 595           boolform))
 596       ; x xor y => ((not x) and y) or ((not y) and x)
 597       ((eq op *xor-op*)
 598         (let (boolform)
 599           (setf boolform
 600             (simp-or
 601               (simp-and (simp-not (first args)) (second args))
 602               (simp-and (simp-not (second args)) (first args))))
 603           (setf args (cddr args))
 604           (loop while args do
 605             (setf boolform
 606               (simp-or
 607                 (simp-and (simp-not boolform) (car args))
 608                 (simp-and (simp-not (car args)) boolform)))
 609             (setf args (cdr args)))
 610           boolform))
 611       (op (apply-op op args))
 612       (t expr))))
 613
 614 (defun $boolean_form (expr)
 615   (boolean-basis-substitute expr))
 616
 617 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 618
 619 ; De Morgan's rules
 620 (defun $demorgan (expr)
 621   (let
 622     ((op (get-maxima-operator expr)) args)
 623     (setf args (if op (mapcar '$demorgan (cdr expr)) nil))
 624     (cond
 625       ((eq op *not-op*)
 626         (let ((op-op (get-maxima-operator (car args))))
 627           (cond
 628             ((eq op-op *and-op*) (apply 'simp-or (mapcar 'simp-not (cdar args))))
 629             ((eq op-op *or-op*) (apply 'simp-and (mapcar 'simp-not (cdar args))))
 630             (t (apply 'simp-not args)))))
 631       ((null op) expr)
 632       (t (apply-op op args)))))
 633
 634 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 635
 636 ; Perfect disjunctive normal forms
 637
 638 (defun elementary-conjunct-disjunct (vars-vals b)
 639   (if (null vars-vals)
 640     nil
 641     (cons
 642       (if (eq (cdar vars-vals) b)
 643         (caar vars-vals)
 644         (list (list *not-op* 'simp) (caar vars-vals)))
 645       (elementary-conjunct-disjunct (cdr vars-vals) b))))
 646
 647 (defun pdnf-pcnf (expr b)
 648   (let ((args (list-of-variables expr)))
 649     (if (null args)
 650       expr
 651       (let (vals (n (length args)) (result nil))
 652         (setf vals (mapcar #'(lambda (l) (zip args l)) (all-charfuns n)))
 653         (loop while vals do
 654           (if (eq (logic-simp (subst-recursive expr (car vals))) b)
 655             (setf result
 656               (cons
 657                 (apply (if b 'simp-and 'simp-or)
 658                   (elementary-conjunct-disjunct (car vals) b))
 659                 result)))
 660           (setf vals (cdr vals)))
 661         (apply  (if b 'simp-or 'simp-and) result)))))
 662
 663 ; Perfect disjunctive normal form
 664 (defun $pdnf (expr)
 665   (pdnf-pcnf expr t))
 666
 667 ; Perfect conjunctive normal form
 668 (defun $pcnf (expr)
 669   (pdnf-pcnf expr nil))
 670
 671 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;