Proof planning is a novel knowledge-based approach for proof construction, which supports the incorporation of mathematical
knowledge and the common mathematical proof techniques of a particular mathematical field.
The diagonalization proof technique is a well-known method in theoretical computer science and in mathematics that originated
with Cantor, who used it to show his seminal uncountability results. It is now widely used as a proof technique for unsolvability
results and metamathematical arguments.
In this paper we give an account on how to systematically construct and plan diagonalization proofs: (i) by finding an indexing
relation, (ii) by constructing a diagonal element, and (iii) by making the implicit contradiction of the diagonal element
explicit. We suggest a declarative representation of the strategy and describe how it is realized in the proof planning environment
of the Ω
mega-System.