Analogies between Proofs : A Case Study

Abstract

This case study examines in detail the theorems and proofs that are shown by analogy in a mathematical textbook on semigroups and automata, that is widely used as an undergraduate textbook in theoretical computer science at German universities (P. Deussen, Halbgruppen und Automaten, Springer 1971). The study shows the important rôle of restructuring a proof for finding analogous subproofs, and of reformulating a proof for the analogical transformation. It also emphasizes the importance of the relevant assumptions of a known proof, i.e., of those assumptions actually used in the proof. In this document we show the theorems, the proof structure, the sub-problems and the proofs of subproblems and their analogues with the purpose to provide an empirical test set of cases for automated analogy-driven theorem proving. Theorems and their proofs are given in natural language augmented by the usual set of mathematical symbols in the studied textbook. As a first step we encode the theorems in logic and show the actual restructuring. Secondly, we code the proofs in a Natural Deduction calculus such that a formal analysis becomes possible and mention reformulations that are necessary in order to reveal the analogy.