The Mechanization of the Diagonalization Proof Strategy

Abstract

We present an empirical study of mathematical proofs by diagonalization, the aim is their mechanization based on proof planning techniques. We show that these proofs can be constructed according to a strategy that (i) finds an indexing relation, (ii) constructs a diagonal element, and (iii) makes the implicit contradiction of the diagonal element explicit. Moreover we suggest how diagonal elements can be represented.