Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-41453
Titel: Completion and Equational Theorem Proving using Taxonomic Constraints
VerfasserIn: Denzinger, Jörg
Sprache: Englisch
Erscheinungsjahr: 1995
Erscheinungsort: Kaiserslautern
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: We present an approach to prove several theorems in slightly different axiom systems simultaneously. We represent the different problems as a taxonomy, i.e. a tree in which each node inherits all knowledge of its predecessors, and solve the problems using inference steps on rules and equations with simple constraints, i.e. words identifying nodes in the taxonomy. We demonstrate that a substantial gain can be achieved by using taxonomic constraints, not only by avoiding the repetition of inference steps in the different problems but also by achieving run times that are much shorter than the accumulated run times when proving each problem separately.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-414530
hdl:20.500.11880/37790
http://dx.doi.org/10.22028/D291-41453
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 95,11
Datum des Eintrags: 5-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-95-11_Denzinger_Completion-and-Equational-Theorem-Proving-using-Taxonomic-Constraints .pdf2,49 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.