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.

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
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
Tag:problem formulation ; resolution; tactics ; theorem proving
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:004 Datenverarbeitung; Informatik

$Rev: 12793 $