Tool to refactor boolean expressions

Question

I'm looking for a tool to refactor boolean expression. I've got expressions like

a1 => (b1 <=> c or d) AND 
a2 => (b2 <=> c or d) AND
a2 => (b2 <=> c or d)

The tool should be able to simplify expressions, e.g. extract the sub expression "c or d" in the example above. Is there a free computer algebra system which can do this?

Currently I think of refactoring the expressions manually an prove the equivalence with a little haskell quickcheck script.

Answer 1

I'm not sure about a tool but take a look at Boolean Algebra

you can draw a grid of all the inputs and output to try and find a minimal boolean expression

Answer 2

The DMS Software Reengineering Tookit could do this.

It is generalized compiler technology for parsing languages (including Java) to ASTs and symbol tables. DMS also provides source-to-source transformations, and associative and commutative law rewriting.

Your boolean expressions would show up as Java AST expression trees. By providing a set of rules about boolean algebra, you can manipulate those expression trees.

We have done this in the past to carry out boolean expression simplification and transformation for C, RLL and a system of diagnostic equations, both on large scale expressions, and on lots of medium scale expressions (scale much like your example).

EDIT 5/19/2010: See an example of conventional algebra transformations using DMS. Its trivial to construct a variant that does Boolean algebra instead.