AN APPROACH TO ANALOGICAL THEOREM-PROVING

This paper proposes an analogical theorem proving method based on intuitionistic type theory. In our research of analogical reasoning applied to automated theorem proving, we feel one of the crucial issues is the proof representation. Usually, proofs and the propositions to be proved are represented in different notations. This impels us to expand analogy relations in two different levels. This is not only cumbersome, but also makes difficult the verification of the analogically obtained target proof. We propose to represent theories, theorems, and proofs in a single formalism. In this framework, we discuss the analogical derivation of proofs from similar ones. Finally, some examples are given to illustrate our method.