Simplifying interpreted formulas

A method is presented for converting a decision procedure for unquantified formulas in an arbitrary first-order theory to a simplifier for such formulas. Given a quantifier-free d.n.f. formula, the method produces a simplest (according to a given criterion) d.n.f. equivalent from among all formulas with atoms in the original formula. The method is predicated on techniques for minimizing purely boolean expressions in the presence of "don't-care" conditions. The don't-cares are used to capture the semantics of the interpreted literals in the formula to be simplified.Two procedures are described: a primitive version of the method that advances the fundamental idea, and a more refined version intended for practical use. Complexity issues are discussed, as is a nontrivial example illustrating the utility of the method.