Abstract
The paper presents sound and complete translations of several fragments of Martin-Löf's monomorphic type theory to first order predicate calculus. The translations are optimised for the purpose of automated theorem proving in the mentioned fragments. The implementation of the theorem prover Gandalf and several experimental results are described.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Peter Aczel. The strength of Martin-Löf's type theory with one universe. In Proceedings of the Symposium on Mathematical Logic, Oulu, 1974, pages 1–32. Report No 2, Department of Philosophy, University of Helsinki, 1977.
L. Augustsson, T. Coquand, and B. Nordström. A short description of Another Logical Framework. In Proceedings of the First Workshop on Logical Frameworks, Antibes, pages 39–42, 1990.
H. Barendregt. The Lambda Calculus. North Holland, 1981.
T.Tammet C.Fermüller, A.Leitsch and N.Zamov. Resolution Methods for the Decision Problem, volume 679 of Lecture Notes in Artificial Intelligence. Springer-Verlag, Berlin Heidelberg, 1993.
C.Green. Application of theorem-proving to problem solving. In Proc. 1st Internat. Joint. Conf. Artificial Intelligence, pages 219–239, 1969.
C.L.Chang and R.C.T Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.
Thierry Coquand. Pattern matching with dependent types. In Proceeding from the logical framework workshop at Båstad, June 1992.
Thierry Coquand, Bengt Nordström, Jan M. Smith, and Björn von Sydow. Type theory and programming. EATCS, 52, February 1994.
A. Felty and D. Miller. Encoding a Dependent-type λ-Calculus in a Logic Programming Language. In Proceedings of CADE-10. Lecture Notes in Artificial Intelligence 449, Springer Verlag, 1990.
G.Peterson. A technique for establishing completeness results in theorem proving with equality. SIAM J. of Comput, 12:82–100, 1983.
Lena Magnusson. The new Implementation of ALF. In The informal proceeding from the logical framework workshop at Båstad, June 1992, 1992.
D. Miller. Proofs in Higher Order Logics. Ph.D. thesis, Carnegie Mellon University, 1983.
D. Miller. A compact representation of proofs. Studia Logica, 46(4), 1987.
G. Mints. Gentzen-type systems and resolution rules. part i. propositional logic. In COLOG-88, volume 417 of Lecture Notes in Computer Science, pages 198–231. Springer Verlag, 1990.
G. Mints. Resolution strategies for the intuitionistic logic. In Constraint Programming, volume 131 of NATO ASI Series F, pages 289–311. Springer Verlag, 1994.
Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf's Type Theory. An Introduction. Oxford University Press, 1990.
Jan Smith. An interpretation of Martin-Löf's type theory in a type-free theory of propositions. Journal of Symbolic Logic, 49(3):730–753, 1984.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tammet, T., Smith, J.M. (1996). Optimized encodings of fragments of type theory in first order logic. In: Berardi, S., Coppo, M. (eds) Types for Proofs and Programs. TYPES 1995. Lecture Notes in Computer Science, vol 1158. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61780-9_75
Download citation
DOI: https://doi.org/10.1007/3-540-61780-9_75
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61780-8
Online ISBN: 978-3-540-70722-6
eBook Packages: Springer Book Archive