Proof Transformation Towards Human Reasoning Style

Abstract

This paper describes the first component of a text planner, which accepts a Gentzen style natural deduction proof and produces a message sequence for the tactical language generator. It first raises the input proofs to the human reasoning level. The main observation is that human inference steps usually have the “size” of the application of an axiom or a theorem. Considered formally, these inference steps can be carried out by domain-specific compound inference rules. An algorithm is developed to generate these rules from axioms and theorems of any particular mathematical theory. Then another algorithm will raise the input proofs using these rules.