Planning Diagonalization Proofs

Abstract

This report is a first attempt of formalizing the diagonalization proof technique. We give a strategy how to systematically construct diagonalization proofs: (i) finding an indexing relation, (ii) constructing a diagonal element, and (iii) making the implicit contradiction of the diagonal element explicit. We suggest a declarative representation of the strategy and describe how it can be realized in a proof planning environment.