Skip to main content
SpringerLink
Log in
Book cover

International Conference on Mathematical Knowledge Management

MKM 2003: Mathematical Knowledge Management pp 188–202Cite as

Comparing Mathematical Provers

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2594))

Abstract

We compare fifteen systems for the formalizations of mathematics with the computer. We present several tables that list various properties of these programs. The three main dimensions on which we compare these systems are: the size of their library, the strength of their logic and their level of automation.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Agerholm, I. Beylin, and P. Dybjer. A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. In TPHOLs’96, volume 1125 of LNCS, pages 17–32. Springer-Verlag, 1996.

    Google Scholar 

  2. S. Agerholm and M.J.C. Gordon. Experiments with ZF Set Theory in HOL and Isabelle. In 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, volume 971, pages 32–45. Springer-Verlag, 1995.

    Google Scholar 

  3. Henk Barendregt. The impact of the lambda calculus. Bulletin of Symbolic Logic, 3(2), 1997.

    Google Scholar 

  4. Henk Barendregt and Herman Geuvers. Proof-Assistants Using Dependent Type Systems. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science Publishers B.V., 2001.

    Google Scholar 

  5. D. Basin and M. Kaufmann. The Boyer-Moore Prover and NuPRL: An experimental comparison. In Proceedings of the First Workshop on ‘Logical Frameworks’, Antibes, France, pages 89–119. Cambridge University Press, 1991.

    Google Scholar 

  6. R. Boyer et al. The QED Manifesto. In A. Bundy, editor, Automated Deduction-CADE 12, volume 814 of LNAI, pages 238–251. Springer-Verlag, 1994. <http://www.cs.kun.nl/~freek/qed/qed.ps.gz>.

  7. B. Buchberger, T. Jebelean, F. Kriftner, M. Marin, and D. Vasaru. An Overview on the Theorema project. In W. Kuechlin, editor, Proceedings of ISSAC’97 (International Symposium on Symbolic and Algebraic Computation), Maui, Hawaii, 1997. ACM Press.

    Google Scholar 

  8. Robert L. Constable, Stuart F. Allen, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, Douglas J. Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, James T. Sasaki, and Scott F. Smith. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, NJ, 1986.

    Google Scholar 

  9. Ingo Dahn and Christoph Wernhard. First Order Proof Problems Extracted from an Article in the MIZAR Mathematical Library. In Proceedings of the International Workshop on First order Theorem Proving, number 97–50 in RISC-Linz Report Series, pages 58–62, Linz, 1997. Johannes Kepler Universität.

    Google Scholar 

  10. G.P. Goold, editor. Selections illustrating the history of Greek mathematics, with an English translation by Ivor Thomas. Harvard University Press, London, 1939.

    Google Scholar 

  11. David Griffioen and Marieke Huisman. A comparison of PVS and Isabelle/HOL. In Jim Grundy and Malcolm Newey, editors, Theorem Proving in Higher Order Logics: 11th International Conference, TPHOLs’98, volume 1479 of LNCS, pages 123–142. Springer-Verlag, 1998.

    Chapter  Google Scholar 

  12. L. Jakubiec, S. Coupet-Grimal, and P. Curzon. A Comparison of the Coq and HOL Proof Systems for Specifying Hardware. In E. Gunter and A. Felty, editors, International Conference on Theorem Proving in Higher Order Logics: B-Track, pages 63–78, 1997.

    Google Scholar 

  13. Matt Kaufmann, Panagiotis Manolios, and J. Strother Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Boston, 2000.

    Book  Google Scholar 

  14. Norman D. Megill. Metamath, A Computer Language for Pure Mathematics. <http://metamath.org/>, 1997.

  15. M. Muzalewski. An Outline of PC Mizar. Fondation Philippe le Hodey, Brussels, 1993. <http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz>.

  16. P. Naumov, M.-O. Stehr, and J. Meseguer. The HOL/NuPRL Proof Translator: A Practical Approach to Formal Interoperability. In R.J. Boulton and P.B. Jackson, editors, The 14th International Conference on Theorem Proving in Higher Order Logics, volume 2152 of LNCS, pages 329–345. Springer-Verlag, 2001.

    MATH  Google Scholar 

  17. R.P. Nederpelt, J.H. Geuvers, and R.C. de Vrijer. Selected Papers on Automath, volume 133 of Studies in Logic and the Foundations of Mathematics. Elsevier Science, Amsterdam, 1994.

    Chapter  Google Scholar 

  18. S. Owre, J. Rushby, and N. Shankar. PVS: A prototype verification system. In D. Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of LNAI, pages 748–752, Berlin, Heidelberg, New York, 1992. Springer-Verlag.

    Google Scholar 

  19. Henri Poincaré. La Science et l’Hypothèse. Flammarion, Paris, 1902.

    Google Scholar 

  20. A. Quaife. Automated Development of Fundamental Mathematical Theories. Kluwer Academic, 1992.

    Google Scholar 

  21. N. Shankar. Metamathematics, Machines and Gödel’s Proof. Number 38 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1994.

    Google Scholar 

  22. Otto Töplitz. The Calculus: A Genetic Approach. University of Chicago Press, Chicago, 1963. Translated by Luise Lange.

    Google Scholar 

  23. F. Wiedijk. Mizar: An Impression. <http://www.cs.kun.nl/~freek/mizar/mizar intro.ps.gz >, 1999.

Download references

Author information

Authors and Affiliations

  1. University of Nijmegen, Nijmegen, The Netherlands

    Freek Wiedijk

Authors
  1. Freek Wiedijk
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Bologna, Mura Anteo Zamboni, 7, 40127, Bologna, Italy

    Andrea Asperti

  2. Research Institute for Symbolic Computation, Johannes Kepler University, 4232 Castle of Hagenberg, Austria

    Bruno Buchberger

  3. Departments of Mathematical Sciences and Computer Science, University of Bath, BA2 7AY, Bath, England

    James Harold Davenport

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Wiedijk, F. (2003). Comparing Mathematical Provers. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds) Mathematical Knowledge Management. MKM 2003. Lecture Notes in Computer Science, vol 2594. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36469-2_15

Download citation

  • DOI: https://doi.org/10.1007/3-540-36469-2_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00568-1

  • Online ISBN: 978-3-540-36469-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation