Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-41580
Titel: | Towards Full Automation of Deduction : A Case Study |
VerfasserIn: | Fuchs, Matthias |
Sprache: | Englisch |
Erscheinungsjahr: | 1996 |
Erscheinungsort: | Kaiserslautern |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | We present first steps towards fully automated deduction that merely requires the user to submit proof problems and pick up results. Essentially, this necessitates the automation of the crucial step in the use of a deduction system, namely choosing 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 integration 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 based on condensed detachment. Our experiments with a fully automated deduction system 'AutoCoDe' have produced remarkable results. We substantiate AutoCoDe's encouraging achievements with a comparison with the renowned theorem prover OTTER. AutoCoDe outperforms OTTER even when assuming very favorable conditions for OTTER. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-415806 hdl:20.500.11880/37825 http://dx.doi.org/10.22028/D291-41580 |
Band: | 96,7 |
Datum des Eintrags: | 6-Jun-2024 |
Fakultät: | SE - Sonstige Einrichtungen |
Fachrichtung: | SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz |
Professur: | SE - Sonstige |
Sammlung: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Dateien zu diesem Datensatz:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
SEKI-Report-SR-96-07_Fuchs_Towards-Full-Automation-of-Deduction-A-Case-Study.pdf | 1,57 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.