TY  - INPR
A1  - Kerber, Manfred
A1  - Präcklein, Axel
T1  - Tactics for the Improvement of Problem Formulation in Resolution-Based Theorem Proving
N2  - 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.
T3  - SEKI Report - 92,9 
KW  - problem formulation
KW  - theorem proving
KW  - tactics
KW  - resolution
Y1  - 1999
UR  - https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/335
UR  - https://nbn-resolving.org/urn:nbn:de:hbz:386-kluedo-3065
ER  -