Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-41422
Titel: | Goal oriented equational theorem proving using team work |
VerfasserIn: | Denzinger, Jörg Fuchs, Matthias |
Sprache: | Englisch |
Erscheinungsjahr: | 1994 |
Erscheinungsort: | Kaiserslautern |
Freie Schlagwörter: | automated theorem proving distributed deduction goal oriented completion |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | The team work method is a concept for distributing automated theorem provers and so to activate several experts to work on a given problem. We have implemented this for pure equational logic using the unfailing Knuth-Bendix completion procedure as basic prover. In this paper we present three classes of experts working in a goal oriented fashion. In general, goal oriented experts perform their job ”unfair” and so are often unable to solve a given problem alone. However, as a team member in the team work method they perform highly efficient, even in comparison with such respected provers as Otter 3.0 or REVEAL, as we demonstrate by examples, some of which can only be proved using team work. The reason for these achievements results from the fact that the team work method forces the experts to compete for a while and then to cooperate by exchanging their best results. This allows one to collect “good” intermediate results and to forget “useless” ones. Completion based proof methods are frequently regarded to have the disadvantage of being not goal oriented. We believe that our approach overcomes this disadvantage to a large extend. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-414226 hdl:20.500.11880/37725 http://dx.doi.org/10.22028/D291-41422 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 94,4 |
Datum des Eintrags: | 28-Mai-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-94-04_Denzinger-Fuchs_Goal-oriented-equational-theorem-proving-using-team-work .pdf | 2,15 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.