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ößeFormat 
SEKI-Report-SR-96-07_Fuchs_Towards-Full-Automation-of-Deduction-A-Case-Study.pdf1,57 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.