Translating machine-generated resolution proofs into ND-proofs at the assertion level

Abstract

Most automated theorem provers suffer from the problem that the resulting proofs are difficult to understand even for experienced mathematicians. Therefore, efforts have been made to transform machine generated proofs (e.g. resolution proofs) into natural deduction (ND) proofs. The state-of-the-art procedure of proof transformation follows basically its completeness proof: the premises and the conclusion are decomposed into unit literals, then the theorem is derived by multiple levels of proofs by contradiction. Indeterminism is introduced by heuristics that aim at the production of more elegant results. This indeterministic character entails not only a complex search, but also leads to unpredictable results.

In this paper we first study resolution proofs in terms of meaningful operations employed by human mathematicians, and thereby establish a correspondence between resolution proofs and ND proofs at a more abstract level. Concretely, we show that if its unit initial clauses are CNFs of literal premises of a problem, a unit resolution corresponds directly to a well-structured ND proof segment that mathematicians intuitively understand as the application of a definition or a theorem. The consequence is twofold: First it enhances our intuitive understanding of resolution proofs in terms of the vocabulary with which mathematicians talk about proofs. Second, the transformation process is now largely deterministic and therefore efficient. This determinism also guarantees the quality of resulting proofs.