Please use this identifier to cite or link to this item:
doi:10.22028/D291-39691 | Title: | Structuring Computer Generated Proofs |
| Author(s): | Lingenfelder, Christoph |
| Language: | English |
| Year of Publication: | 1988 |
| Place of publication: | Kaiserslautern |
| DDC notations: | 004 Computer science, internet |
| Publikation type: | Report |
| Abstract: | One of the main disadvantages of computer generated proofs of mathematical theorems is their complexity and incomprehensibility. 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. During this process topological properties of the refutation graphs can be successfully exploited in order to obtain structured proofs. It is also possible to remove trivial steps from the proof formulation . |
| Link to this record: | urn:nbn:de:bsz:291--ds-396910 hdl:20.500.11880/36029 http://dx.doi.org/10.22028/D291-39691 |
| Series name: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
| Series volume: | 88,19 |
| Date of registration: | 23-Jun-2023 |
| Faculty: | SE - Sonstige Einrichtungen |
| Department: | SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz |
| Professorship: | SE - Sonstige |
| Collections: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Files for this record:
| File | Description | Size | Format | |
|---|---|---|---|---|
| SEKI-Report-SR-88-19_Lingenfelder_Structuring-Computer-Generated-Proofs.pdf | 22,96 MB | Adobe PDF | View/Open |
Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.