Abstract
The old idea that proofs are in some sense functions, has been made precise by the Curry-Howard-correspondence between proofs in natural deduction and terms in typed λ-calculus. Since the latter can be viewed as an idealized functional programming language, this amounts to an interpretation of proofs as functional programs. This concept and related ones going back to work of Gentzen, Gödel, Kleene and Kreisel are implemented in Minlog, an interactive proof system designed for generating proof terms and exploring their algorithmic content. Besides tools for interactive proof generation, Minlog has automatic devices
-
to search for purely logical (sub)proofs,
-
to check the correctness of a proof,
-
to remove detours in a proof,
-
to make a nonconstructive proof constructive,
-
to read off witnesses from a constructive proof,
-
to adapt an already existing proof to special cases,
-
to produce a legible verbalization from a formal proof.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Berger, U.: 1993a, `Program Extraction from Classical Proofs’. In: D. Leivant (ed.): Logic and Computational Complexity, LCC ‘84, Vol. 960 of Lecture Notes in Computer Science. pp. 77–97, Springer Verlag, Berlin, Heidelberg, New York.
Berger, U.: 1993b, `Program Extraction from Classical Proofs’. In: D. Leivant (ed.): Logic and Computational Complexity, LCC ‘84, Vol. 960 of Lecture Notes in Computer Science. pp. 91–117
Berger, U., M. Eberl, and H. Schwichtenberg: 1998, `Normalization by evaluation’. Submitted to: B. Möller and J.V. Tucker (eds.): Prospects for hardware foundations. NADA volume, Lecture Notes in Computer Science.
Berger, U. and H. Schwichtenberg: 1991, `An inverse of the evaluation functional for typed A-calculus’. In: R. Vemuri (ed.): Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science. pp. 203–211, IEEE Computer Society Press, Los Alamitos.
Berger, U. and H. Schwichtenberg: 1995, `Program Extraction from Classical Proofs’. In: D. Leivant (ed.): Logic and Computational Complexity, LCC ‘84, Vol. 960 of Lecture Notes in Computer Science. pp. 77–97, Springer Verlag, Berlin, Heidelberg, New York.
Boyer, R. S. and J. S. Moore: 1988, A Computational Logic Handbook, Vol. 23 of Perspectives in Computing. Academic Press, Inc.
Friedman, H.: 1978, `Classically and intuitionistically provably recursive functions’. In: D. Scott and G. Müller (eds.): Higher Set Theory, Vol. 669 of Lecture Notes in Mathematics. pp. 21–28, Springer Verlag, Berlin, Heidelberg, New York.
Goad, C. A.: 1980, `Computational uses of the manipulation of formal proofs’. Ph.D. thesis, Stanford University. Stanford Department of Computer Science Report No. STAN-CS-80–819.
Hayashi, S.: 1990, `An introduction to PX’. In: G. Huet (ed.): Logical Foundations of Functional Programming. Addison-Wesley, pp. 432–486.
Kreisel, G.: 1959, `Interpretation of analysis by means of constructive functionals of finite types’. In: A. Heyting (ed.): Constructivity in Mathematics. North-Holland, Amsterdam, pp. 101–128.
Leivant, D.: 1985, `Syntactic Translations and Provably Recursive Functions’. The Journal of Symbolic Logic 50 (3), 682–688.
Miller, D.: 1991, `A logic programming language with lambda-abstraction, function variables and simple unification’. Journal of Logic and Computation 1(4), 497536.
Nipkow, T.: 1993, `Orthogonal Higher-Order Rewrite Systems are Confluent’. In: M. Bezem and J. Groote (eds.): Typed Lambda Calculi and Applications, Vol. 664 of Lecture Notes in Computer Science. pp. 306–317, Springer Verlag, Berlin, Heidelberg, New York.
Scott, D.: 1982, `Domains for denotational semantics’. In: E. Nielsen and E. Schmidt (eds.): Automata, Languages and Programming, Vol. 140 of Lecture Notes in Computer Science. pp. 577–613, Springer Verlag, Berlin, Heidelberg, New York.
Tait, W. W.: 1967, `Intensional Interpretations of Functionals of Finite Type I’. The Journal of Symbolic Logic 32 (2), 198–212.
Troelstra, A. S. and D. van Dalen: 1988, Constructivism in Mathematics. An Introduction, Vol. 121, 123 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam.
Turner, R.: 1991, Constructive Foundations for functional languages. McGraw-Hill. van de Pol, J. and H. Schwichtenberg: 1995, `Strict functionals for termination proofs’. In: M. Dezani-Ciancaglini and G. Plotkin (eds.): Typed Lambda Calculi and Applications, Vol. 902 of Lecture Notes in Computer Science. pp. 350–364, Springer Verlag, Berlin, Heidelberg, New York.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Benl, Berger, Schwichtenberg, Seisenberger, Zuber (1998). Proof Theory at Work: Program Development in the Minlog System. In: Bibel, W., Schmitt, P.H. (eds) Automated Deduction — A Basis for Applications. Applied Logic Series, vol 9. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-0435-9_2
Download citation
DOI: https://doi.org/10.1007/978-94-017-0435-9_2
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5051-9
Online ISBN: 978-94-017-0435-9
eBook Packages: Springer Book Archive