share/logic/logic.dem

   1 /*
   2  * logic.mac--Logic algebra package for Maxima CAS.
   3  * Copyright (c) 2008--2009 Alexey Beshenov <al@beshenov.ru>.
   4  *
   5  * Version 2.1. 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 load ("logic.mac")$
  25
  26 logic_simp (a or (b or false or (a or b)));
  27 logic_simp (b eq a eq false eq true);
  28 logic_simp ((a xor true) xor b xor true);
  29 logic_simp ((a implies q) or (not (a implies q)) or b);
  30
  31 characteristic_vector (true);
  32 characteristic_vector (a xor b);
  33 characteristic_vector (a implies b);
  34 characteristic_vector (a implies b, a, b);
  35 characteristic_vector (a implies b, b, a);
  36
  37 zhegalkin_form (a or b or c);
  38 zhegalkin_form ((a implies b) or c);
  39
  40 e : ((a or b) xor c) and d$
  41 ezh : zhegalkin_form (e);
  42 logic_equiv (ezh, e);
  43 is (characteristic_vector(ezh) = characteristic_vector(e));
  44 logic_equiv (x and y eq x, x implies y);
  45
  46 dual_function (x or y);
  47 zhegalkin_form (%);
  48
  49 self_dual (a);
  50 self_dual (not a);
  51 self_dual (a eq b);
  52
  53 closed_under_f (x and y);
  54 closed_under_f (x or y);
  55 closed_under_t (x and y);
  56 closed_under_t (x or y);
  57
  58 monotonic (a or b);
  59 monotonic (a and b);
  60 monotonic (a implies b);
  61 monotonic (a xor b);
  62
  63 linear (a or b);
  64 linear (a eq b);
  65
  66 functionally_complete (x and y, x xor y);
  67 functionally_complete (x and y, x xor y, true);
  68 functionally_complete (x and y, x or y, not x);
  69
  70 logic_basis (x and y, x or y, not x);
  71 logic_basis (x and y, not x);
  72 logic_basis (x or y, not x);
  73
  74 logic_functions : { not x, x nand y, x nor y,
  75                     x implies y, x and y, x or y,
  76                     x eq y, x xor y, true, false }$
  77 logic_bases : subset (powerset(logic_functions), lambda ([s], apply ('logic_basis, listify(s))));
  78
  79 logic_diff (a or b or c, a);
  80 logic_diff (a and b and c, a);
  81 logic_diff (true, a);
  82
  83 boolean_form (a implies b implies c);
  84 demorgan (%);
  85 logic_equiv (boolean_form (a implies b implies c), zhegalkin_form (a implies b implies c));
  86
  87 demorgan (boolean_form (a nor b nor c));
  88
  89 pdnf (x implies y);
  90 pcnf (x implies y);
  91 logic_equiv (pdnf (x implies y), pcnf (x implies y));