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.
Publication Year: 1989
Publication Date: 1989-08-20
Language: en
Type: article
Access and Citation
Cited By Count: 31
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot