Transformation and Structuring of Computer Generated Proofs

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.