Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-41423
Titel: | Analysis and Representation of Equational Proofs Generated by a Distributed Completion Based Proof System |
VerfasserIn: | Denzinger, Jörg Schulz, Stephan |
Sprache: | Englisch |
Erscheinungsjahr: | 1994 |
Erscheinungsort: | Kaiserslautern |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | Automatic proof systems are becoming more and more powerful. However, the proofs generated by these systems are not met with wide acceptance, because they are presented in a way inappropriate for human understanding. In this paper we pursue two different, but related, aims. First we describe methods to structure and transform equational proofs in a way that they conform to human reading conventions. We develop algorithms to impose a hierarchical structure on proof protocols from completion based proof systems and to generate equational chains from them. Our second aim is to demonstrate the difficulties of obtaining such protocols from distributed proof systems and to present our solution to these problems for provers using the TEAMWORK method. We also show that proof systems using this method can give considerable help in structuring the proof listing in a way analogous to human behaviour. In addition to theoretical results we also include descriptions on algorithms, implementation notes, examples and data on a variety of examples. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-414234 hdl:20.500.11880/37733 http://dx.doi.org/10.22028/D291-41423 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 94,5 |
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-05_Denzinger-Schulz_Analysis-and-Representation-of-Equational-Proofs-Generated-by-a-Distributed-Completion-Based-Proof-System.pdf | 4,66 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.