Reformulating Resolution Problems by Tactics
Manfred Kerber, Axel Präcklein · 1999
A straightforward formulation of a mathematical problem is mostly not adequate for resolution theorem proving. We present a method to optimize such formulations by exploiting the variability of first-order logic. The optimizing transformation is described as logic morphisms, whose operationalizations are tactics. The different behaviour of a resolution theorem prover for the source and target formulations is demonstrated by several examples. It is shown how tactical and resolution-style theorem proving can be combined. Keywords: problem formulation, resolution, tactics, theorem proving. 1 Introduction Solving mathematical problems with resolution-based theorem proving systems requires, in most cases, intelligence and ingenuity on the part of the user, since the final formulation of the problem is of essential importance for the problem-solving behaviour of the system. Often the main job is to formulate the task in a machinefriendly form, and once this is done, the system easily finds...