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



Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.