Gray-Box Proving in Theorema

Many theorems in mathematics have the form of an implication, an equivalence, or an equality, and in the standard prover in the Theorema system such formulas are handled by rewriting. Definitions of new function- or predicate symbols are yet another example of formulas that require rewriting in their treatment in the Theorema system. Both theorems and definitions in practice often carry conditions under which they are valid. Rewriting is, thus, only valid in cases where all side-conditions are met. On the other hand, many of these side-conditions are trivial and when presenting a proof we do not want to distract the reader with lengthy derivations that justify the side-conditions. The goal of this paper is to present the design and implementation of a mechanism that efficiently checks side-conditions in rewriting while preserving the readability and the explanatory power of a mathematical proof, which has always been of central interest in the development of the Theorema system.