Applications of inductive definitions and choice principles to
program synthesis
Ulrich Berger and Monika Seisenberger
Abstract
We describe two methods of extracting constructive content from
classical proofs, focusing on theorems involving infinite sequences
and nonconstructive choice principles. The first method removes any
reference to infinite sequences and transforms the theorem into a
system of inductive definitions, the other applies a combination of
Gödel's negative- and Friedman's A-translation. Both approaches
are explained by means of a case study on Higman's Lemma and its
well-known classical proof due to Nash-Williams. We also discuss some
proof-theoretic optimizations that were crucial for the formalization
and implementation of this work in the interactive proof system
Minlog.
Bib entry
Draft copy:
[pdf]
[ps]