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
Additional Services
| 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 |
