1(kill(all), 'done);
2'done$
3
4(load("logic.lisp"), 'done);
5'done$
6
7logic_simp (a or (b or false or (a or b)));
8a or b$
9
10logic_simp (b eq a eq false eq true);
11a eq b eq false$
12
13logic_simp ((a xor true) xor b xor true);
14a xor b$
15
16characteristic_vector (f(x,y,z), x, y, z);
17[f(false,false,false),f(false,false,true),f(false,true,false),
18 f(false,true,true),f(true,false,false),f(true,false,true),f(true,true,false),
19 f(true,true,true)]$
20
21characteristic_vector (true);
22[true]$
23
24characteristic_vector (a xor b);
25[false, true, true, false]$
26
27characteristic_vector (a implies b);
28[true, true, false, true]$
29
30characteristic_vector (a implies b, a, b);
31[true, true, false, true]$
32
33characteristic_vector (a implies b, b, a);
34[true, false, true, true]$
35
36zhegalkin_form (a or b or c);
37a and b and c xor a and b xor a and c xor b and c xor a xor b xor c$
38
39zhegalkin_form ((a implies b) or c);
40a and b and c xor a and b xor a and c xor a xor true$
41
42block([e, f],
43  e : ((a or b) xor c) and d, f: zhegalkin_form (e),
44  [logic_equiv (e, f), is(characteristic_vector(e)=characteristic_vector(f))]);
45[true, true]$
46
47logic_equiv (x and y eq x, x implies y);
48true$
49
50demorgan(dual_function (x or y));
51x and y$
52
53self_dual (a);
54true$
55
56self_dual (not a);
57true$
58
59self_dual (a eq b);
60false$
61
62closed_under_f (x and y);
63true$
64
65closed_under_f (x or y);
66true$
67
68closed_under_t (x and y);
69true$
70
71closed_under_t (x or y);
72true$
73
74monotonic (a or b);
75true$
76
77monotonic (a and b);
78true$
79
80monotonic (a implies b);
81false$
82
83characteristic_vector (a or b);
84[false, true, true, true]$
85
86characteristic_vector (a and b);
87[false, false, false, true]$
88
89characteristic_vector (a implies b);
90[true, true, false, true]$
91
92characteristic_vector (a xor b);
93[false, true, true, false]$
94
95linear(a or b);
96false$
97
98linear(a eq b);
99true$
100
101zhegalkin_form (a or b);
102(a and b) xor a xor b$
103
104zhegalkin_form (a eq b);
105a xor b xor true$
106
107functionally_complete (x and y, x xor y);
108false$
109
110functionally_complete (x and y, x xor y, true);
111true$
112
113functionally_complete (x and y, x or y, not x);
114true$
115
116logic_basis (x and y, x or y);
117false$
118
119logic_basis (x and y, x or y, not x);
120false$
121
122logic_basis (x and y, not x);
123true$
124
125logic_basis (x or y, not x);
126true$
127
128logic_basis (x and y, x xor y, true);
129true$
130
131block([logic_functions : { not x, x nand y, x nor y,
132                                    x implies y, x and y, x or y,
133                                    x eq y, x xor y, true, false }],
134                                    subset (powerset(logic_functions),
135                                      lambda ([s], apply ('logic_basis, listify(s)))));
136{{false, x eq y, x and y}, {false, x eq y, x or y},
137{false, x implies y}, {true, x xor y, x and y},
138{true, x xor y, x or y}, {not x, x implies y},
139{not x, x and y}, {not x, x or y},
140{x eq y, x xor y, x and y}, {x eq y, x xor y, x or y},
141{x implies y, x xor y}, {x nand y}, {x nor y}}$
142
143logic_diff (a or b or c, a);
144(b and c) xor b xor c xor true$
145
146logic_diff (a and b and c, a);
147b and c$
148
149logic_diff (a or (not a), a);
150false$
151
152demorgan(boolean_form (a implies b implies c));
153((not b) and a) or c$
154
155logic_equiv (boolean_form (a implies b implies c),
156  zhegalkin_form (a implies b implies c));
157true$
158
159demorgan (boolean_form (a nor b nor c));
160(not a) and (not b) and (not c)$
161
162pdnf (x implies y);
163(x and y) or ((not x) and y) or ((not x) and (not y))$
164
165pcnf (x implies y);
166(not x) or y$
167