• search hit 1 of 1
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

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