Alexey,
This looks great! Much useful functionality.
I have also been working on logical simplification (with contributions
from Barton Willis), and I have running Lisp code for the basic
simplifications in the form of simplifying functions. As standard
simplifying functions, they work correctly for (e.g.) subst(a,b,a AND
b) => a. The Lisp package should also be much faster because it avoids
the overhead of the pattern-matcher and Maxima code, and because it
uses better algorithms in some cases.
On the other hand, I have not been working on the more advanced
algorithms such as change of basis, normal forms, etc.
Like you, I've been keeping my logical operators distinct from
Maxima's built-in operators to avoid the integration issues but we
also need to address that at some point....
I suspect that the right way forward is to use my Lisp code for
simplification and your code for the more advanced functionality.
-s
PS A few bugs I've encountered in your code: a AND f(a) => error; a
AND a[1] => a[1]; (a XOR NOT a) and (a EQ NOT a) don't simplify; 1 AND
3 => 3 (should either be an error if only 0 and 1 are booleans r
should be 1 if bitwise); a<b AND c parses as a<(b AND c) -- binding
powers aren't correct; (a AND f(a)) and logicdiff(f(x),x) => error
(should be noun form -- this is apparently because you are using EV,
which is always dangerous).