Fred: an implementation of a layered approach to extracting programs from proofs. Part I: an application in graph theory

In this paper we describe our system Fred for automatically extracting "correct" programs from proofs using a development of the Curry-Howard process. Although program extraction has been developed by many authors (see [5, 2, 8]), our system has a number of novel features designed to make it very easy to use and as close as possible to ordinary mathematical terminology and practice. These features include 1. the use of Henkin's technique [6] to reduce higher-order logic to many-sorted (first-order) logic 2. the free use of new rules for induction subject to certain conditions 3. the extensive use of previously programmed (primitive) recursive functions 4. the use of templates to make the reasoning much closer to normal mathematical proofs. 5. an extension of the technique of the use of Harrop formulae to classically true formulae (cf. the footnote on p.101 in Kreisel [10]). As an example of our system we give a constructive proof of the well-known theorem that every graph of even parity can be decomposed into a list of disjoint cycles. Given such a graph as input, the extracted program produces a list of such cycles as promised.