Tactics for the Improvement of Problem Formulation in Resolution-Based Theorem Proving
Manfred Kerber, Axel Präcklein · Publication Server of Kaiserslautern University of Technology (Kaiserslautern University of Technology) · 1992
We transform a user-friendly formulation of aproblem to a machine-friendly one exploiting the variabilityof first-order logic to express facts. The usefulness of tacticsto improve the presentation is shown with several examples.In particular it is shown how tactical and resolution theoremproving can be combined.