Abstract
Automated theorem provers for first order logic have reached a state where they can give useful support for interactive theorem proving. However, most real world problems handled in interactive theorem proving are formulated in a typed language. First order provers have currently rather limited capabilities to handle types. Therefore type information has to be encoded in an efficient way. What is most efficient, depends on the type system as well as on the first order prover at hand.
Supported by the Deutsche Forschungsgemeinschaft
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
K. J. Barwise: Axioms for abstract model theory; Ann. Math. Logic vol. 7 (1974), 221–265
I. Dahn, C. Wernhard: First Order Proof Problems Extracted from an Article in the MIZAR Mathematical Library. RISC-Linz Report Series, No. 97-50, pp. 58–62, Johannes Kepler Universität Linz, 1997.
B. I. Dahn, J. Gehne, Th. Honigmann, A. Wolf: Integration of Automated and Interactive Theorem Proving in Ilf. In Proc. CADE-14, pp. 57–60, Springer, 1997.
H. Ganzinger, C. Meyer, C. Weidenbach: Soft Typing for Ordered Resolution. In Proc. CADE-14, pp. 321–335, Springer, 1997.
Mellish, C. S.: Implementing Systemic Classification by Unification. Comp. Ling. 14, 1988, pp 40–51
The Mizar Library Committee: Syntax of the Mizar Language. http://www.mizar.org/language/syntax.txt
P. Rudnicki: An Overview of the Mizar Project. Proceedings of the 1992 Workshop on Types for Proofs and Programs, Chalmers University of Technology, Bastad 1992.
A. Tarski “Uber unerreichbare Kardinalzahlen, Fund. Math., vol.30 (1938), pp.68–69
A. Trybulec: Some Features of the Mizar Language, ESPRIT Workshop, Torino 1993.
G. Wiederhold, M. Genesereth: The Basis for Mediation. To appear IEEE Expert
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dahn, I. (2000). Interpretation of a Mizar-Like Logic in First Order Logic. In: Caferra, R., Salzer, G. (eds) Automated Deduction in Classical and Non-Classical Logics. FTP 1998. Lecture Notes in Computer Science(), vol 1761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46508-1_9
Download citation
DOI: https://doi.org/10.1007/3-540-46508-1_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67190-9
Online ISBN: 978-3-540-46508-9
eBook Packages: Springer Book Archive