Hi Richard,
1) I think the first question here to be considered is how
pure propositional logic, that is, boolean variables (where
e.g. a<b is treated such a variable) and connections and, or, not,
is to be handled.
Which "normal form"?
There are various normal forms (e.g., DNF, CNF, ROBBD's, AIG's, sum-of-product),
some are canonical, some not, but I think one should stay within the class
of propositional expressions (otherwise we get strange "terms", which can
not be easily read).
It seems most natural now to use what was introduced by Archie Blake in 1937,
and runs under various names, e.g., Blake canonical form, namely the disjunction
of all prime implicants. Then two expressions are equivalent iff their normal
forms are equal.
Sure, propositional expressions have in general exponentially long Blake
canonical forms, but that can't be avoided.
2) Then comes the question of extending this basic propositional
logic by "understanding" equality/disequality.
Here the natural environment seems what is typically called the
theory of equality with uninterpreted functions (EUF).
Validity in this fragment of first-order logic is decided by the
congruence-closure algorithm.
This would not work by replacing a formula with an equivalent
normal form (which is kind of nice), but it uses a decision algorithm
for valid formulas (for example: (x=y and f(x) # f(y)) is equal to false).
3) Finally EUF is extended by < and <=, obtaining the (quantifier-free)
first-order theory of (arbitrary) linear orders (with function symbols and
equality). Since it's quantifier-free, we still have a reasonably efficient
decision procedure (though at the moment I don't have a source for it).
Using external solvers (typically in C++) would be easiest (they exist,
also as open-source programs). It would be nice if Maxima would use
such extensions (some time ago we also discussed the inclusion of
the QEPCAD system, which would be a great addition to Maxima's
reasoning power).
Oliver
On Fri, Dec 16, 2011 at 04:49:17PM -0500, Richard Hennessy wrote:
> Hi List;
>
> Does anyone know what it would take to implement a Boolean algebra package for
> Maxima? I have been thinking of doing this for while but I am not sure where
> to start. Any helpful links would be nice. I was planning on allowing just
> the following types of predicates:
>
> P(a,b):= a < b;
> P(a,b):= a <= b;
> P(a,b):= a > b;
> P(a,b):= a >= b;
> P(a,b):= equal(a, b);
> P(a,b):= notequal(a, b);
>
> along with the three connecters ?and?, ?or? and ?not?.
>
> so you could do stuff like
>
> if a<m or a >= m then cos(x) else sin(x);
>
> This would just simplify to cos(x), currently it does not simplify. More
> complex conditionals are obviously possible.
>
> I don?t know much about what it would take to do this or if it is too hard, or
> too much work. I have studied logic design, so I know about some
> simplifications of Booleans, but this whole idea is a little scary to take on
> without some help.
>
> Richard Hennessy
>
>