This article generalises the refined A-translation method for extracting programs from classical proofs [U. Berger,W. Buchholz, H. Schwichtenberg, Refined program extraction from classical proofs, Annals of Pure and Applied Logic 114 3–25] to the scenario where additional assumptions such as choice principles are involved. In the case of choice principles, this is done by adding computational content to the ‘translated’ assumptions, an idea which goes back to [S. Berardi, M. Bezem, T. Coquand, On the computational content of the axiom of (...) choice, JSL 63 600–622] and has been further elaborated in [U. Berger, P. Oliva, Modified bar recursion and classical dependent choice, in: M. Baaz, S.D. Friedman, J. Kraijcek , Logic Colloquium ’01, in: Lecture Notes in Logic, vol. 20, Springer, Berlin, 2005, pp. 89–107]. We further investigate the applicability of this extension by means of a small but non-trivial example, and discuss the formalisation as well as some optimisations necessary in order to extract terminating programs. Both formalisation and term extraction have been implemented in the interactive proof assistant Minlog. (shrink)

We upgrade the light Dialectica interpretation [6] by adding two more light universal quantifiers, which are both semi-computational and semi-uniform and complement each other. An illustrative example is presented for the new light quantifiers and a new application is given for the older uniform quantifier. The realizability of new light negative formulations for the Axiom of Choice and for the Independence of Premises is explored in the new setting.

In view of an enhancement of our implementation on the computer, we explore the possibility of an algorithmic optimization of the various proof-theoretic techniques employed by Kohlenbach for the synthesis of new effective uniform bounds out of established qualitative proofs in Numerical Functional Analysis. Concretely, we prove that the method of “colouring” some of the quantifiers as “non-computational” extends well to ε-arithmetization, elimination-of-extensionality and model-interpretation.

From a classical proof that the gcd of natural numbers a1 and a2 is a linear combination of the two, we extract by Gödel's Dialectica interpretation an algorithm computing the coefficients. The proof uses the minimum principle. We show generally how well-founded recursion can be used to Dialectica interpret well-founded induction, which is needed in the proof of the minimum principle. In the special case of the example above it turns out that we obtain a reasonable extracted term, representing an (...) algorithm close to Euclid's. (shrink)

Let A be a formula without implications, and Γ consist of formulas containing disjunction and falsity only negatively and implication only positively. Orevkov and Nadathur proved that classical derivability of A from Γ implies intuitionistic derivability, by a transformation of derivations in sequent calculi. We give a new proof of this result , where the input data are natural deduction proofs in long normal form involving stability axioms for relations; the proof gives a quadratic algorithm to remove the stability axioms. (...) This can be of interest for computational uses of classical proofs. (shrink)

We present an extension of Heyting arithmetic in finite types called Uniform Heyting Arithmetic that allows for the extraction of optimized programs from constructive and classical proofs. The system has two sorts of first-order quantifiers: ordinary quantifiers governed by the usual rules, and uniform quantifiers subject to stronger variable conditions expressing roughly that the quantified object is not computationally used in the proof. We combine a Kripke-style Friedman/Dragalin translation which is inspired by work of Coquand and Hofmann and a variant (...) of the refined A-translation due to Buchholz, Schwichtenberg and the author to extract programs from a rather large class of classical first-order proofs while keeping explicit control over the levels of recursion and the decision procedures for predicates used in the extracted program. (shrink)