Structuring Computer Generated Proofs

Lingenfelder, Christoph

Structuring Computer Generated Proofs

Download BibTeX Cite

Proceedings of the Eleventh International Joint Conference on Artificial Intelligence. Automated Deduction. 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.

Christoph Lingenfelder. 1989. Structuring Computer Generated Proofs. In Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, IJCAI-89. IJCAI, 378–382. https://ijcai.org/proceedings/1989/60

@inproceedings{ijcai1989p60,
  title     = {Structuring Computer Generated Proofs},
  author    = {Lingenfelder, Christoph},
  booktitle = {Proceedings of the Eleventh International Joint Conference on
               Artificial Intelligence, {IJCAI-89}},
  publisher = {International Joint Conferences on Artificial Intelligence},
  editor    = {N. S. Sridharan},
  pages     = {378--382},
  year      = {1989},
  month     = {8},
  note      = {Automated Deduction},
  url       = {https://ijcai.org/proceedings/1989/60},
}

TY  - CPAPER
TI  - Structuring Computer Generated Proofs
AU  - Lingenfelder, Christoph
T2  - Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, IJCAI-89
PB  - International Joint Conferences on Artificial Intelligence
PY  - 1989
SP  - 378
EP  - 382
UR  - https://ijcai.org/proceedings/1989/60
ER  -