Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-40274
Titel: | Transformation and Structuring of Computer Generated Proofs |
VerfasserIn: | Lingenfelder, Christoph |
Sprache: | Englisch |
Erscheinungsjahr: | 1990 |
Erscheinungsort: | Kaiserslautern |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | One of the main disadvantages of computer generated proofs of mathematical theorems is often their complexity and incomprehensibility. This is even more of a problem for the presentation of inferences drawn by automated reasoning components in other AI systems. Proof transformation procedures have been designed in order to state these proofs in a formalism that is more familiar to a human mathematician. But usually the essential idea of a proof is still not easily visible. We describe a procedure to transform proofs represented as abstract refutation graphs into natural deduction proofs with a special emphasis on an “intelligent” selection of inference rules. In particular the frequent use of proofs by contradiction is avoided. During this process topological properties of the refutation graphs can be successfully exploited in order to obtain well-structured proofs. This is accomplished by dividing a large proof into a set of hierarchically arranged subproofs which are more easily comprehensible. This may be achieved by formulating lemmata that are then applied more than once in the subsequent proof, but also by simply inserting subgoals or by breaking up a substantial part of a proof into a case analysis. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-402741 hdl:20.500.11880/36216 http://dx.doi.org/10.22028/D291-40274 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 90,26 |
Datum des Eintrags: | 11-Aug-2023 |
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-90-26_Lingenfelder_Transformation-and-Structuring-of-Computer-Generated-Proofs.pdf | 6,71 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.