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.
Volltext Dateien herunterladen
Weitere Dienste
| Verfasser*innenangaben: | Manfred Kerber, Axel Präcklein |
|---|---|
| URN: | urn:nbn:de:hbz:386-kluedo-3065 |
| Schriftenreihe (Bandnummer): | SEKI Report (92,9) |
| Dokumentart: | Preprint |
| Sprache der Veröffentlichung: | Englisch |
| Jahr der Fertigstellung: | 1999 |
| Jahr der Erstveröffentlichung: | 1999 |
| Veröffentlichende Institution: | Technische Universität Kaiserslautern |
| Datum der Publikation (Server): | 03.04.2000 |
| Freies Schlagwort / Tag: | problem formulation; resolution; tactics; theorem proving |
| Fachbereiche / Organisatorische Einheiten: | Kaiserslautern - Fachbereich Informatik |
| DDC-Sachgruppen: | 0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik |
| Lizenz (Deutsch): |  Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011 |