• search hit 1 of 4
Back to Result List

Tactics for the Improvement of Problem Formulation in Resolution-Based Theorem Proving

  • 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.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Author:Manfred Kerber, Axel Präcklein
URN (permanent link):urn:nbn:de:hbz:386-kluedo-3065
Serie (Series number):SEKI Report (92,9)
Document Type:Preprint
Language of publication:English
Year of Completion:1999
Year of Publication:1999
Publishing Institute:Technische Universität Kaiserslautern
Date of the Publication (Server):2000/04/03
Tag:problem formulation; resolution; tactics; theorem proving
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011