Abstract
In this paper, we show that an intuitionistic logic with second-order function quantification, called hh 2 here, can serve as a meta-language to directly and naturally specify both sequent calculi and natural deduction inference systems for first-order logic. For the intuitionistic subset of first-order logic, we present a set of hh 2 formulas which simultaneously specifies both kinds of inference systems and provides a direct and concise account of the correspondence between cut-free sequential proofs and normal natural deduction proofs. The logic of hh 2 can be implemented using such logic programming techniques as providing operational interpretations to the connectives and implementing unification on λ-terms. With respect to such an interpreter, our specification provides a description of how to convert a proof in one system to a proof in the other. The operation of converting a sequent proof to a natural deduction proof is functional in the sense that there is always one natural deduction proof corresponding to each sequent proof. Our specification, in fact, provides a direct implementation of the transformation in this direction.
Preview
Unable to display preview. Download preview PDF.
References
Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.
Michael Dummett. Elements of Intuitionism. Clarendon Press, Oxford, 1977.
Conal Elliott and Frank Pfenning. eLP, a Common Lisp Implementation of λProlog. May 1989.
Amy Felty. Specifying and Implementing Theorem Provers in a Higher-Order Logic Programming Language. PhD thesis, University of Pennsylvania, August 1989.
Amy Felty and Dale Miller. Specifying theorem provers in a higher-order logic programming language. In Ninth International Conference on Automated Deduction, Argonne Ill., May 1988.
Gerhard Gentzen. Investigations into logical deductions, 1935. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68–131, North-Holland Publishing Co., Amsterdam, 1969.
J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinatory Logic and Lambda Calculus. Cambridge University Press, 1986.
Gérard Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.
Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. To appear in the Annals of Pure and Applied Logic.
Gopalan Nadathur and Dale Miller. Higher-order horn clauses. April 1988. To appear in the Journal of the ACM.
Gopalan Nadathur and Dale Miller. An overview of λProlog. In K. Bowen and R. Kowalski, editors, Fifth International Conference and Symposium on Logic Programming, MIT Press, 1988.
Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5(3):363–397, September 1989.
Garrel Pottinger. Normalization as a homomorphic image of cut-elimination. Annals of Mathematical Logic, 12(3):223–357, 1977.
Dag Prawitz. Ideas and results in proof theory. In J.E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pages 235–307, North-Holland, Amsterdam, 1971.
Dag Prawitz. Natural Deduction. Almqvist & Wiksell, Uppsala, 1965.
J. I. Zucker. Cut-elimination and normalization. Annals of Mathematical Logic, 1(1):1–112, 1974.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Felty, A. (1991). A logic program for transforming sequent proofs to natural deduction proofs. In: Schroeder-Heister, P. (eds) Extensions of Logic Programming. ELP 1989. Lecture Notes in Computer Science, vol 475. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0038694
Download citation
DOI: https://doi.org/10.1007/BFb0038694
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53590-4
Online ISBN: 978-3-540-46879-0
eBook Packages: Springer Book Archive