---
title: "Structuring Computer Generated Proofs"
authors:
  - "Christoph Lingenfelder"
doi: ""
url: "https://ijcai.org/proceedings/1989/60"
pdf: "https://ijcai.org/proceedings/1989/0060.pdf"
venue: "Proceedings of the Eleventh International Joint Conference on Artificial Intelligence"
year: 1989
pages: "378-382"
track: "Automated Deduction"
keywords:
---

# Structuring Computer Generated Proofs

Christoph Lingenfelder

*Proceedings of the Eleventh International Joint Conference on Artificial Intelligence*, pages 378-382.

## 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 exploited in order to obtain structured proofs.