Towards Full Automation of Deduction: A Case Study
- We present first steps towards fully automated deduction that merely requiresthe user to submit proof problems and pick up results. Essentially, this necessi-tates the automation of the crucial step in the use of a deduction system, namelychoosing and configuring an appropriate search-guiding heuristic. Furthermore,we motivate why learning capabilities are pivotal for satisfactory performance.The infrastructure for automating both the selection of a heuristic and integra-tion of learning are provided in form of an environment embedding the "core"deduction system.We have conducted a case study in connection with a deduction system basedon condensed detachment. Our experiments with a fully automated deductionsystem 'AutoCoDe' have produced remarkable results. We substantiate Au-toCoDe's encouraging achievements with a comparison with the renowned the-orem prover Otter. AutoCoDe outperforms Otter even when assuming veryfavorable conditions for Otter.
Author: | Matthias Fuchs |
---|---|
URN: | urn:nbn:de:hbz:386-kluedo-3640 |
Series (Serial Number): | SEKI Report (96,7) |
Document Type: | Preprint |
Language of publication: | English |
Year of Completion: | 1996 |
Year of first Publication: | 1996 |
Publishing Institution: | Technische Universität Kaiserslautern |
Date of the Publication (Server): | 2000/04/03 |
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 |