USING TACTICS TO REFORMULATE FORMULAS FOR RESOLUTION THEOREM-PROVING

We present a method to optimize formulations of mathematical problems by exploiting the variability of first-order logic. The optimizing tra nsformation is described as logic morphisms, whose operationalizations are tactics. The different behaviour of a resolution theorem prover f or the source and target formulations is demonstrated by several examp les. Such tactics give a user the possibility to formally manipulate p roblem formulations.