In a previous paper [LR1] we presented a theoretical model
for propositional Boolean algebras,
based on techniques from Commutative Algebra.

It was adapted to check the forward reasoning consistency of a given
Knowledge Based System (KBS) based on bivalent logic [LR2].
Surprisingly, verification is usually hand made, for example
``visually", with the help of diagrams.

The paper below begins with a brief resume of those results.
A brand new implementation based in Maple V is described afterwards.
This description pays special attention to the algebraic details of
the implementation. The procedures are given in full detail.

There is a great advantage with respect to working just with rewriting
techniques, such as those used in
Maple's ``Logic package". To approach the problem
using ideals and class rings makes it possible
to go further and directly modelize the algebra associated to a KBS
as a polynomial Boolean algebra (that is also a k-algebra).

Sun Apr 23 10:32:10 MDT 1995