Refined program extraction from classical proofs. (English) Zbl 0992.03070
Summary: The paper presents a refined method of extracting reasonable and sometimes unexpected programs from classical proofs of formulas of the form \(\forall x\exists yB\). We also generalize previously known results, since \(B\) no longer needs to be quantifier-free, but only has to belong to a strictly larger class of so-called “good formulas”. Furthermore, we allow unproven lemmas \(D\) in the proof of \(\forall x\exists yB\), where \(D\) is a so-called “definite” formula.
MSC:
| 03F10 | Functionals in proof theory |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03F50 | Metamathematics of constructive systems |
References:
| [1] | Barbanera, F.; Berardi, S., Extracting constructive content from classical logic via control-like reductions, (Bezem, M.; Groote, J. F., Typed Lambda Calculi and Applications. Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, vol. 664 (1993), Springer: Springer Berlin), 45-59 · Zbl 0788.68016 |
| [2] | U. Berger, Programs from classical proofs, in: M. Behara, R. Fritsch, R.G. Lintz (Eds.), Symposia Gaussiana, Proc. 2nd Gauss Symp., Conf. A: Mathematics and Theoretical Physics. Munich, Germany, August 2-7, 1993, Walter de Gruyter, Berlin, 1995, pp. 187-200.; U. Berger, Programs from classical proofs, in: M. Behara, R. Fritsch, R.G. Lintz (Eds.), Symposia Gaussiana, Proc. 2nd Gauss Symp., Conf. A: Mathematics and Theoretical Physics. Munich, Germany, August 2-7, 1993, Walter de Gruyter, Berlin, 1995, pp. 187-200. · Zbl 0848.03029 |
| [3] | U. Berger, H. Schwichtenberg, Program extraction from classical proofs, in: D. Leivant (Ed.), Logic and Computational Complexity, International Workshop LCC’94, Indianapolis, IN, USA, October 1994, Lecture Notes in Computer Science, vol. 960, Springer, Berlin, 1995, pp. 77-97.; U. Berger, H. Schwichtenberg, Program extraction from classical proofs, in: D. Leivant (Ed.), Logic and Computational Complexity, International Workshop LCC’94, Indianapolis, IN, USA, October 1994, Lecture Notes in Computer Science, vol. 960, Springer, Berlin, 1995, pp. 77-97. · Zbl 1540.03018 |
| [4] | Berger, U.; Schwichtenberg, H.; Seisenberger, M., The Warshall algorithm and Dickson’s lemmatwo examples of realistic program extraction, J. Automat. Reason., 26, 205-221 (2001) · Zbl 0958.03009 |
| [5] | Constable, R. L.; Murthy, C., Finding computational content in classical proofs, (Huet, G.; Plotkin, G., Logical Frameworks (1991), Cambridge University Press: Cambridge University Press Cambridge), 341-362 · Zbl 0754.03040 |
| [6] | Coquand, T.; Persson, H., Gröbner basis in type theory., (Altenkirch, T.; Naraschewski, W.; Reus, B., Types for Proofs and Programs. Types for Proofs and Programs, Lecture Notes in Computer Science, vol. 1657 (1999), Springer: Springer New York) |
| [7] | Dickson, L. E., Finiteness of the odd perfect and primitive abundant numbers with \(n\) distinct prime factors, Am. J. Math., 35, 413-422 (1913) · JFM 44.0220.02 |
| [8] | Felleisen, M.; Friedman, D. P.; Kohlbecker, E.; Duba, B. F., A syntactic theory of sequential control, Theoret. Comput. Sci., 52, 205-237 (1987) · Zbl 0643.03011 |
| [9] | Felleisen, M.; Hieb, R., The revised report on the syntactic theory of sequential control and state, Theoret. Comput. Sci., 102, 235-271 (1992) · Zbl 0764.68094 |
| [10] | Friedman, H., Classically and intuitionistically provably recursive functions, (Scott, D. S.; Müller, G. H., Higher Set Theory. Higher Set Theory, Lecture Notes in Mathematics, vol. 669 (1978), Springer: Springer Berlin), 21-28 · Zbl 0396.03045 |
| [11] | T.G. Griffin, A formulae-as-types notion of control, in: Conf. Record 17th Annu. ACM Symp. on Principles of Programming Languages, 1990, pp. 47-58.; T.G. Griffin, A formulae-as-types notion of control, in: Conf. Record 17th Annu. ACM Symp. on Principles of Programming Languages, 1990, pp. 47-58. |
| [12] | Kohlenbach, U., Analysing proofs in analysis, (Hodges, W.; Hyland, M.; Steinhorn, C.; Truss, J., Logic: from Foundations to Applications. European Logic Colloquium (Keele, 1993) (1996), Oxford University Press: Oxford University Press Oxford), 225-260 · Zbl 0881.03032 |
| [13] | Krivine, J.-L., Classical logic, storage operators and second-order lambda-calculus, Ann. Pure Appl. Logic, 68, 53-78 (1994) · Zbl 0814.03009 |
| [14] | Leivant, D., Syntactic translations and provably recursive functions, J. Symbolic Logic, 50, 3, 682-688 (1985) · Zbl 0593.03038 |
| [15] | C. Murthy, Extracting constructive content from classical proofs, Technical Report 90-1151, Ph.D. Thesis, Department of Computer Science, Cornell University, Ithaca, New York, 1990.; C. Murthy, Extracting constructive content from classical proofs, Technical Report 90-1151, Ph.D. Thesis, Department of Computer Science, Cornell University, Ithaca, New York, 1990. |
| [16] | M. Parigot, \(λμ\); M. Parigot, \(λμ\) · Zbl 0925.03092 |
| [17] | (Troelstra, A. S., Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lecture Notes in Mathematics, vol. 344 (1973), Springer: Springer Berlin) · Zbl 0275.02025 |
| [18] | Troelstra, A. S.; van Dalen, Dirk, Constructivism in Mathematics, An Introduction. Constructivism in Mathematics, An Introduction, Studies in Logic and the Foundations of Mathematics, vols. 121 and 123 (1988), North-Holland: North-Holland Amsterdam · Zbl 0661.03047 |
| [19] | Bezem, M.; Veldman, W., Ramsey’s theorem and the pigeonhole principle in intuitionistic mathematics, J. London Math. Soc., 47, 193-211 (1993) · Zbl 0729.03034 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
