Translating Mizar for First Order Theorem Provers

  • Josef Urban
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2594)


The constructor system of the Mizar proof checking system is explained here on examples from Mizar articles,and its translation to untyped first-order syntax is described and discussed.This makes the currently largest library of formalized mathematics available to first- order theorem provers.


Theorem Prover Aggregate Type Type Hierarchy Constructor Level Order Translation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Belinfante 96]
    Johan Belinfante, On a Modification of Godel’s Algorithm for Class Formation, Association for Automated Reasoning Newsletter, No.34,pp.1015 (1996)]Google Scholar
  2. [Bonarska 90]
    Bonarska, E., An Introduction to PC Mizar, Fondation Ph.le Hodey, Brussels,1990.Google Scholar
  3. [Dahn 98]
    Ingo Dahn. Interpretation of a Mizar-like Logic in First Order Logic. Proceedings of FTP 1998.pp.137–151.Google Scholar
  4. [Goguen 92]
    J. Goguen and J. Meseguer. Order-sorted algebra I:Equational deduction formultiple inheritance,overloading,exceptions and partial operations. Theoretical Computer Science, 105(2): 217–273, 1992.MathSciNetCrossRefGoogle Scholar
  5. [Hahnle et all 96]
    R. Hahnle, M. Kerber, and C. Weidenbach. Common Syntax of the DFGSchwerpunktprogramm Deduction.Technical Report TR 10/96, Fakultät für Informatik,Universät Karlsruhe, Karlsruhe, Germany,1996.Google Scholar
  6. [McCune 94]
    McCune, W. W., OTTER 3.0 Reference Manual and Guide, Technical Report ANL-94/6, Argonne National Laboratory, Argonne, Illinois (1994).Google Scholar
  7. [Muzalewski 93]
    Muzalewski, M., An Outline of PC Mizar, Fondation Philippe le Hodey, Brussels, 1993.Google Scholar
  8. [REAL.
    1]_Krzysztof Hryniewiecki, Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.Google Scholar
  9. [Rudnicky 92]
    Rudnicki, P., An Overview of the Mizar Project, Proceedings of the 1992 Workshop on Types for Proofs and Programs, Chalmers University of Technology, Bastad, 1992.Google Scholar
  10. [Schumann 2001]
    J. M. Schumann, Automated Theorem-Proving in Software Engineering. Springer-Verlag, 2001.Google Scholar
  11. [Suttner and Sutcliffe 98]
    C. Suttner and G. Sutcliffe. The TPTP problem library (TPTP v2.2.0). Technical Report 9704, Department of Computer Science, James Cook University, Townsville, Australia,1998.Google Scholar
  12. [Weidenbach et all 99]
    Weidenbach C., Afshordel B., Brahm U., Cohrs C., Engel T., Keen R., Theobalt C.and Topic D., System description:Spass version 1.0.0, in H. Ganzinger, ed., ‘16th International Conference on Automated Deduction,CADE-16”, Vol. 1632 of LNAI, Springer, pp 314–318Google Scholar
  13. [Wiedijk 99 ]
    Freek Wiedijk. Mizar:An impression. Unpublished paper,1999.

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Josef Urban
    • 1
  1. 1.Dept.of Theoretical Computer ScienceCharles UniversityPrahaCzech Republic

Personalised recommendations