share/logic/logic.texi

   1 \input texinfo
   2
   3 @c logic.mac--Logic algebra package for Maxima CAS.
   4 @c Copyright (c) 2008--2009 Alexey Beshenov <al@beshenov.ru>.
   5 @c
   6 @c Version 2.1. Last modified 2009-01-07
   7 @c
   8 @c logic.mac is free software; you can redistribute it and/or modify it
   9 @c under the terms of the GNU Lesser General Public License as published
  10 @c by the Free Software Foundation; either version 2.1 of the License,
  11 @c or (at your option) any later version.
  12 @c
  13 @c logic.mac is distributed in the hope that it will be useful, but
  14 @c WITHOUT ANY WARRANTY; without even the implied warranty of
  15 @c MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
  16 @c General Public License for more details.
  17 @c
  18 @c You should have received a copy of the GNU General Public License
  19 @c along with the logic.mac; see the file COPYING. If not, write to the
  20 @c Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
  21 @c Boston, MA 02110-1301, USA.
  22
  23 @c Remove the empty page before a new chapter.
  24 @setchapternewpage off
  25
  26 @setfilename logic.info
  27 @settitle logic
  28
  29 @ifinfo
  30 @macro var {expr}
  31 <\expr\>
  32 @end macro
  33 @end ifinfo
  34
  35 @dircategory Mathematics/Maxima
  36 @direntry
  37 * logic: (maxima/logic).           Maxima share package logic for operations on Boolean variables.
  38 @end direntry
  39
  40 @node Top, Introduction to logic, (dir), (dir)
  41 @top
  42 @menu
  43 * Introduction to logic::
  44 * Definitions for logic::
  45 * Function and variable index::
  46 @end menu
  47 @chapter logic
  48
  49 @node Introduction to logic, Definitions for logic, Top, Top
  50 @section Introduction to logic
  51
  52 This is a draft version of logic algebra package for Maxima.
  53 It is being developed by Alexey@tie{}Beshenov@tie{}(al@@beshenov.ru).
  54 All source code is available uder the terms of GNU@tie{}GPL@tie{}2.1.
  55
  56 List of recognized operators:
  57
  58 @multitable @columnfractions .15 .10 .10 .45 .2
  59 @headitem Operator @tab Type @tab Binding power @tab Description @tab Properties
  60 @item @code{not}
  61 @tab Prefix
  62 @tab @code{70}
  63 @tab Logical NOT (negation)
  64 @tab
  65 @item @code{and}
  66 @tab N-ary
  67 @tab @code{65}
  68 @tab Logical AND (conjunction)
  69 @tab Commutative
  70 @item @code{nand}
  71 @tab N-ary
  72 @tab @code{62}
  73 @tab Sheffer stroke (alternative denial, NAND)
  74 @tab Commutative
  75 @item @code{nor}
  76 @tab N-ary
  77 @tab @code{61}
  78 @tab Webb-operation or Peirce arrow (Quine's dagger, NOR)
  79 @tab Commutative
  80 @item @code{or}
  81 @tab N-ary
  82 @tab @code{60}
  83 @tab Logical OR (disjunction)
  84 @tab Commutative
  85 @item @code{implies}
  86 @tab Infix
  87 @tab @code{59}
  88 @tab Implication
  89 @tab
  90 @item @code{eq}
  91 @tab N-ary
  92 @tab @code{58}
  93 @tab Equivalence
  94 @tab Commutative
  95 @item @code{xor}
  96 @tab N-ary
  97 @tab @code{58}
  98 @tab Sum modulo 2 (exclusive or)
  99 @tab Commutative
 100 @end multitable
 101
 102
 103 @section @TeX{}@tie{}output
 104
 105 logic.mac assigns the following @TeX{}@tie{}output:
 106
 107 @table @code
 108 @item not
 109 @code{\neg}
 110 @item and
 111 @code{\wedge}
 112 @item nand
 113 @code{\mid}
 114 @item nor
 115 @code{\downarrow}
 116 @item or
 117 @code{\vee}
 118 @item implies
 119 @code{\rightarrow}
 120 @item eq
 121 @code{\sim}
 122 @item xor
 123 @code{\oplus}
 124 @end table
 125
 126 Examples:
 127
 128 @example
 129 (%i1) load ("logic.mac")$
 130 @group
 131 (%i2) tex (a implies b)$
 132 $$a \rightarrow b$$
 133 @end group
 134 @group
 135 (%i3) tex ((a nor b) nand c)$
 136 $$\left(a \downarrow b\right) \mid c$$
 137 @end group
 138 @group
 139 (%i4) tex (zhegalkin_form (a or b or c))$
 140 $$a \wedge b \wedge c \oplus a \wedge b \oplus a \wedge c \oplus b
 141   \wedge c \oplus a \oplus b \oplus c$$
 142 @end group
 143 @group
 144 (%i5) tex (boolean_form (a implies b implies c));
 145 $$ \neg \left( \neg a \vee b\right) \vee c$$
 146 @end group
 147 @group
 148 (%i6) tex (a eq b eq c);
 149 $$a \sim b \sim c$$
 150 @end group
 151
 152 @end example
 153
 154 @tex
 155 $$a \rightarrow b$$
 156 $$\left(a \downarrow b\right) \mid c$$
 157 $$a \wedge b \wedge c \oplus a \wedge b \oplus a \wedge c \oplus b
 158   \wedge c \oplus a \oplus b \oplus c$$
 159 $$ \neg \left( \neg a \vee b\right) \vee c$$
 160 $$a \sim b \sim c$$
 161 @end tex
 162
 163 @node Definitions for logic, Function and variable index, Introduction to logic, Top
 164 @section Definitions for logic
 165
 166 @deffn {Function} logic_simp (@var{expr})
 167
 168 Returns a simplified version of logical expression @var{expr}.
 169
 170 Examples:
 171
 172 @example
 173 (%i1) load ("logic.mac")$
 174 @group
 175 (%i2) logic_simp (a or (b or false or (a or b)));
 176 (%o2)                               a or b
 177 @end group
 178 @group
 179 (%i3) logic_simp (b eq a eq false eq true);
 180 (%o3)                           eq a eq b false
 181 @end group
 182 @group
 183 (%i4) logic_simp ((a xor true) xor b xor true);
 184 (%o4)                               a xor b
 185 @end group
 186 @end example
 187
 188 The function applies only basic simplification rules without introducing new
 189 functions.
 190
 191 N.B. It should be merged somehow with the basic Maxima simplifier.
 192 @end deffn
 193
 194
 195 @deffn {Function} characteristic_vector (@var{expr}, @var{var_1}, ..., @var{var_n})
 196
 197 Returns a list of size @math{2^n} with all possible values of @var{expr}.
 198
 199 For example, @code{characteristic_vector (f(x,y,z), x, y, z)} is equivalent to
 200 list
 201
 202 @example
 203 @group
 204 [
 205   f (false, false, false),
 206   f (false, false,  true),
 207   f (false,  true, false),
 208   f (false,  true,  true),
 209   f ( true, false, false),
 210   f ( true, false,  true),
 211   f ( true,  true, false),
 212   f ( true,  true,  true)
 213 ]
 214 @end group
 215 @end example
 216
 217 If @code{@var{var_1}, ..., @var{var_n}} is omitted, it is assumed that
 218
 219 @example
 220 [@var{var_1}, ..., @var{var_n}] = sort(listofvars(@var{expr}))
 221 @end example
 222
 223 Examples:
 224
 225 @example
 226 (%i1) load ("logic.mac")$
 227 @group
 228 (%i2) characteristic_vector (true);
 229 (%o2)                               [true]
 230 @end group
 231 @group
 232 (%i3) characteristic_vector (a xor b);
 233 (%o3)                     [false, true, true, false]
 234 @end group
 235 @group
 236 (%i4) characteristic_vector (a implies b);
 237 (%o4)                      [true, true, false, true]
 238 @end group
 239 @group
 240 (%i5) characteristic_vector (a implies b, a, b);
 241 (%o5)                      [true, true, false, true]
 242 @end group
 243 @group
 244 (%i6) characteristic_vector (a implies b, b, a);
 245 (%o6)                      [true, false, true, true]
 246 @end group
 247 @end example
 248 @end deffn
 249
 250
 251 @deffn {Function} zhegalkin_form (@var{expr})
 252
 253 Returns the representation of @var{expr} in Zhegalkin basis
 254 @code{@{xor, and, true@}}.
 255
 256 Examples:
 257
 258 @example
 259 (%i1) load ("logic.mac")$
 260 @group
 261 (%i2) zhegalkin_form (a or b or c);
 262 (%o2) (a and b and c) xor (a and b) xor (a and c)
 263                                xor (b and c) xor a xor b xor c
 264 @end group
 265 @group
 266 (%i3) zhegalkin_form ((a implies b) or c);
 267 (%o3) (a and b and c) xor (a and b) xor (a and c) xor a
 268                                                       xor true
 269 @end group
 270 @end example
 271 @end deffn
 272
 273
 274 @deffn {Function} logic_equiv (@var{expr_1}, @var{expr_2})
 275
 276 Returns @code{true} if @var{expr_1} is equivalent to @var{expr_2} and
 277 @code{false} otherwise.
 278
 279 Examples:
 280
 281 @example
 282 (%i1) load ("logic.mac")$
 283 (%i2) e : ((a or b) xor c) and d$
 284 @group
 285 (%i3) zhegalkin_form (e);
 286 (%o3) (a and b and d) xor (a and d) xor (b and d)
 287                                                  xor (c and d)
 288 @end group
 289 @group
 290 (%i4) logic_equiv (%i2, %o3);
 291 (%o4)                                true
 292 @end group
 293 @group
 294 (%i5) is (characteristic_vector(%i2) = characteristic_vector(%o3));
 295 (%o5)                                true
 296 @end group
 297 @group
 298 (%i6) logic_equiv (x and y eq x, x implies y);
 299 (%o6)                                true
 300 @end group
 301 @end example
 302 @end deffn
 303
 304
 305 @deffn {Function} dual_function (@var{expr})
 306
 307 @example
 308 dual_function (f (x_1, ..., x_n)) := not f (not x_1, ..., not x_n).
 309 @end example
 310
 311 Example:
 312
 313 @example
 314 (%i1) load ("logic.mac")$
 315 @group
 316 (%i2) dual_function (x or y);
 317 (%o2)                     not ((not x) or (not y))
 318 @end group
 319 @group
 320 (%i3) demorgan (%);
 321 (%o3)                               x and y
 322 @end group
 323 @end example
 324 @end deffn
 325
 326
 327 @deffn {Function} self_dual (@var{expr})
 328 Returns @code{true} if @var{expr} is equivalent to
 329 @code{dual_function (@var{expr})} and @code{false} otherwise.
 330
 331 Examples:
 332
 333 @example
 334 (%i1) load ("logic.mac")$
 335 @group
 336 (%i2) self_dual (a);
 337 (%o2)                               true
 338 @end group
 339 @group
 340 (%i3) self_dual (not a);
 341 (%o3)                               true
 342 @end group
 343 @group
 344 (%i4) self_dual (a eq b);
 345 (%o4)                               false
 346 @end group
 347 @end example
 348 @end deffn
 349
 350
 351 @deffn {Function} closed_under_f (@var{expr})
 352 @code{closed_under_f (f (x_1, ..., x_n)} returns @code{true} if
 353 @code{f (false, ..., false) = false} and @code{false} otherwise.
 354
 355 Examples:
 356
 357 @example
 358 (%i1) load ("logic.mac")$
 359 @group
 360 (%i2) closed_under_f (x and y);
 361 (%o2)                                true
 362 @end group
 363 @group
 364 (%i3) closed_under_f (x or y);
 365 (%o3)                                true
 366 @end group
 367 @end example
 368 @end deffn
 369
 370
 371 @deffn {Function} closed_under_t (@var{expr})
 372 @code{closed_under_t (f (x_1, ..., x_n)} returns @code{true} if
 373 @code{f (true, ..., true) = true} and @code{false} otherwise.
 374
 375 Examples:
 376
 377 @example
 378 (%i1) load ("logic.mac")$
 379 @group
 380 (%i2) closed_under_t (x and y);
 381 (%o2)                                true
 382 @end group
 383 @group
 384 (%i3) closed_under_t (x or y);
 385 (%o3)                                true
 386 @end group
 387 @end example
 388 @end deffn
 389
 390
 391 @deffn {Function} monotonic (@var{expr})
 392 Returns @code{true} if characteristic vector of @var{expr} is monotonic, i.e.
 393
 394 @example
 395 charvec : characteristic_vector(expr)
 396 charvec[i] <= charvec[i+1],   i = 1, ..., n-1
 397 @end example
 398
 399 where @code{a<=b := (a=b or (a=false and b=true))}.
 400
 401 Examples:
 402
 403 @example
 404 (%i1) load ("logic.mac")$
 405 @group
 406 (%i2) monotonic (a or b);
 407 (%o2)                                true
 408 @end group
 409 @group
 410 (%i3) monotonic (a and b);
 411 (%o3)                                true
 412 @end group
 413 @group
 414 (%i4) monotonic (a implies b);
 415 (%o4)                                false
 416 @end group
 417 @group
 418 (%i5) monotonic (a xor b);
 419 (%o5)                                false
 420 @end group
 421 @group
 422 (%i6) characteristic_vector (a or b);
 423 (%o6)                     [false, true, true, true]
 424 @end group
 425 @group
 426 (%i7) characteristic_vector (a and b);
 427 (%o7)                    [false, false, false, true]
 428 @end group
 429 @group
 430 (%i8) characteristic_vector (a implies b);
 431 (%o8)                     [true, true, false, true]
 432 @end group
 433 @group
 434 (%i9) characteristic_vector (a xor b);
 435 (%o9)                    [false, true, true, false]
 436 @end group
 437 @end example
 438 @end deffn
 439
 440
 441 @deffn {Function} linear (@var{expr})
 442 Returns @code{true} if @code{zhegalkin_form(@var{expr})} is linear and
 443 @code{false} otherwise.
 444
 445 Examples:
 446
 447 @example
 448 (%i1) load ("logic.mac")$
 449 @group
 450 (%i2) linear (a or b);
 451 (%o2)                                false
 452 @end group
 453 @group
 454 (%i3) linear (a eq b);
 455 (%o3)                                true
 456 @end group
 457 @group
 458 (%i4) zhegalkin_form (a or b);
 459 (%o4)              (a and b) xor a xor b
 460 @end group
 461 @group
 462 (%i5) zhegalkin_form (a eq b);
 463 (%o5)                 a xor b xor true
 464 @end group
 465 @end example
 466
 467 Linear functions are also known as counting or alternating functions.
 468 @end deffn
 469
 470
 471 @deffn {Function} functionally_complete (@var{expr_1}, ..., @var{expr_n})
 472 Returns @code{true} if @var{expr_1}, ..., @var{expr_n} is a functionally
 473 complete system and @code{false} otherwise.
 474 The constants are essential (see the example below).
 475
 476 Examples:
 477
 478 @example
 479 (%i1) load ("logic.mac")$
 480 @group
 481 (%i2) functionally_complete (x and y, x xor y);
 482 (%o2)                                false
 483 @end group
 484 @group
 485 (%i3) functionally_complete (x and y, x xor y, true);
 486 (%o3)                                true
 487 @end group
 488 @group
 489 (%i4) functionally_complete (x and y, x or y, not x);
 490 (%o4)                                true
 491 @end group
 492 @end example
 493 @end deffn
 494
 495
 496 @deffn {Function} logic_basis (@var{expr_1}, ..., @var{expr_n})
 497 Returns @code{true} if @var{expr_1}, ..., @var{expr_n} is a functionally
 498 complete system without redundant elements and @code{false} otherwise.
 499
 500 Examples:
 501
 502 @example
 503 (%i1) load ("logic.mac")$
 504 @group
 505 (%i2) logic_basis (x and y, x or y);
 506 (%o2)                       false
 507 @end group
 508 @group
 509 (%i3) logic_basis (x and y, x or y, not x);
 510 (%o3)                       false
 511 @end group
 512 @group
 513 (%i4) logic_basis (x and y, not x);
 514 (%o4)                       true
 515 @end group
 516 @group
 517 (%i5) logic_basis (x or y, not x);
 518 (%o5)                       true
 519 @end group
 520 @group
 521 (%i8) logic_basis (x and y, x xor y, true);
 522 (%o8)                       true
 523 @end group
 524 @end example
 525
 526 All possible bases:
 527
 528 @example
 529 (%i1) load ("logic.mac")$
 530 (%i2) logic_functions : @{ not x, x nand y, x nor y,
 531                           x implies y, x and y, x or y,
 532                           x eq y, x xor y, true, false @}$
 533 @group
 534 (%i3) subset (powerset(logic_functions),
 535               lambda ([s], apply ('logic_basis, listify(s))));
 536 (%o3) @{@{false, x eq y, x and y@}, @{false, x eq y, x or y@},
 537 @{false, x implies y@}, @{true, x xor y, x and y@},
 538 @{true, x xor y, x or y@}, @{not x, x implies y@},
 539 @{not x, x and y@}, @{not x, x or y@},
 540 @{x eq y, x xor y, x and y@}, @{x eq y, x xor y, x or y@},
 541 @{x implies y, x xor y@}, @{x nand y@}, @{x nor y@}@}
 542 @end group
 543 @end example
 544 @end deffn
 545
 546 @deffn {Function} logic_diff (@var{f}, @var{x})
 547 Returns the logic derivative @math{df/dx} of @math{f} wrt @math{x}.
 548
 549 @example
 550 @group
 551 logic_diff (f (x_1, ..., x_k, ..., x_n),  x_k) :=
 552     f (x_1, ..., true, ..., x_n)  xor
 553         f (x_1, ..., false, ..., x_n)
 554 @end group
 555 @end example
 556
 557 Examples:
 558
 559 @example
 560 (%i1) load ("logic.mac")$
 561 @group
 562 (%i2) logic_diff (a or b or c, a);
 563 (%o2)          (b and c) xor b xor c xor true
 564 @end group
 565 @group
 566 (%i3) logic_diff (a and b and c, a);
 567 (%o3)                      b and c
 568 @end group
 569 @group
 570 (%i4) logic_diff (a or (not a), a);
 571 (%o4)                       false
 572 @end group
 573 @end example
 574 @end deffn
 575
 576
 577 @deffn {Function} boolean_form (@var{expr})
 578
 579 Returns the representation of @var{expr} in Boolean basis
 580 @code{@{and, or, not@}}.
 581
 582 Examples:
 583
 584 @example
 585 (%i1) load ("logic.mac")$
 586 @group
 587 (%i2) boolean_form (a implies b implies c);
 588 (%o2)             (not ((not a) or b)) or c
 589 @end group
 590 @group
 591 (%i3) demorgan (%);
 592 (%o3)               ((not b) and a) or c
 593 @end group
 594 @group
 595 (%i4) logic_equiv (boolean_form (a implies b implies c),
 596                    zhegalkin_form (a implies b implies c));
 597 (%o4)                       true
 598 @end group
 599 @end example
 600 @end deffn
 601
 602
 603 @deffn {Function} demorgan (@var{expr})
 604
 605 Applies De Morgan's rules to @var{expr}:
 606
 607 @example
 608 not (x_1 and ... and x_n) => (not x_1  or ...  or not x_n)
 609 not (x_1  or ...  or x_n) => (not x_1 and ... and not x_n)
 610 @end example
 611
 612 Example:
 613
 614 @example
 615 (%i1) load ("logic.mac")$
 616 @group
 617 (%i2) demorgan (boolean_form (a nor b nor c));
 618 (%o2)          (not a) and (not b) and (not c)
 619 @end group
 620 @end example
 621 @end deffn
 622
 623
 624 @deffn {Function} pdnf (@var{expr})
 625
 626 Returns the perfect disjunctive normal form of @var{expr}.
 627
 628 Example:
 629
 630 @example
 631 (%i1) load ("logic.mac")$
 632 @group
 633 (%i2) pdnf (x implies y);
 634 (%o2) (x and y) or ((not x) and y) or ((not x) and (not y))
 635 @end group
 636 @end example
 637 @end deffn
 638
 639
 640 @deffn {Function} pcnf (@var{expr})
 641
 642 Returns the perfect conjunctive normal form of @var{expr}.
 643
 644 Example:
 645
 646 @example
 647 (%i1) load ("logic.mac")$
 648 @group
 649 (%i2) pcnf (x implies y);
 650 (%o2)                   (not x) or y
 651 @end group
 652 @end example
 653 @end deffn
 654
 655 @node Function and variable index,  , Definitions for logic, Top
 656 @appendix Function and variable index
 657 @printindex fn
 658 @c @printindex vr
 659
 660 @bye