Abstract 
: 
We present a method to simplify expressions in the context of a formal, axiomatically defined, the ory. In this paper, equality axioms are typically used but the method is more generally applicable. The key idea of the method is to represent large, even infinite, sets of expressions1 by means of a special data structure that allows us to apply axioms to the sets as a whole, not to single individual expressions. We then propose a bottomup algorithm to finitely compute theories with a finite number of equivalence classes of equal terms. In that case, expressions can be simplified (i.e., minimized) in linear time by “folding” them on the computed representation of the theory. We demonstrate the method for boolean expressions with a small number of variables. Finally, we propose a “goal oriented” algorithm that computes only small parts of the underlying theory, in order to simplify a given particular expression. We show that the algorithm is able to simplify boolean expressions with many more variables but optimality cannot be certified anymore.
[eng] We present a method to simplify expressions in the context of a formal, axiomatically defined, the ory. In this paper, equality axioms are typically used but the method is more generally applicable. The key idea of the method is to represent large, even infinite, sets of expressions1 by means of a special data structure that allows us to apply axioms to the sets as a whole, not to single individual expressions. We then propose a bottomup algorithm to finitely compute theories with a finite number of equivalence classes of equal terms. In that case, expressions can be simplified (i.e., minimized) in linear time by “folding” them on the computed representation of the theory. We demonstrate the method for boolean expressions with a small number of variables. Finally, we propose a “goal oriented” algorithm that computes only small parts of the underlying theory, in order to simplify a given particular expression. We show that the algorithm is able to simplify boolean expressions with many more variables but optimality cannot be certified anymore.
