Skip to main content
SpringerLink
Log in
Book cover

The Seventeen Provers of the World

Foreword by Dana S. Scott

  • Book
  • © 2006

Overview

Editors:
  1. Freek Wiedijk

    1. Institute for Computing and Information Sciences, Radboud University Nijmegen, Nijmegen, The Netherlands

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

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

Part of the book sub series: Lecture Notes in Artificial Intelligence (LNAI)

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

Access this book

Log in via an institution
eBook USD 44.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 59.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

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (19 chapters)

  1. Front Matter

    Download chapter PDF

  2. Introduction

    • Freek Wiedijk
    Pages 1-9

  3. Informal

    • Henk Barendregt
    Pages 10-10

  4. HOL

    • John Harrison, Konrad Slind, Rob Arthan
    Pages 11-19

  5. Mizar

    • Andrzej Trybulec
    Pages 20-23

  6. PVS

    • Bart Jacobs, John Rushby
    Pages 24-27

  7. Coq

    • Laurent Théry, Pierre Letouzey, Georges Gonthier
    Pages 28-35

  8. Otter/Ivy

    • Michael Beeson, William McCune
    Pages 36-40

  9. Isabelle/Isar

    • Markus Wenzel, Larry Paulson
    Pages 41-49

  10. Alfa/Agda

    • Thierry Coquand
    Pages 50-54

  11. ACL2

    • Ruben Gamboa
    Pages 55-66

  12. PhoX

    • Christophe Raffalli, Paul Rozière
    Pages 67-71

  13. IMPS

    • William Farmer
    Pages 72-87

  14. Metamath

    • Norman Megill
    Pages 88-95

  15. Theorema

    • Wolfgang Windsteiger, Bruno Buchberger, Markus Rozenkranz
    Pages 96-107

  16. Lego

    • Conor McBride
    Pages 108-115

  17. Nuprl

    • Paul Jackson
    Pages 116-126

  18. Ωmega

    • Christoph Benzmüller, Armin Fiedler, Andreas Meier, Martin Pollet, Jörg Siekmann
    Pages 127-141

  19. B Method

    • Dominique Cansell
    Pages 142-150

  20. Minlog

    • Helmut Schwichtenberg
    Pages 151-157
Back to top

Keywords

About this book

Commemorating the 50th anniversary of the first time a mathematical theorem was proven by a computer system, Freek Wiedijk initiated the present book in 2004 by inviting formalizations of a proof of the irrationality of the square root of two from scientists using various theorem proving systems.

The 17 systems included in this volume are among the most relevant ones for the formalization of mathematics. The systems are showcased by presentation of the formalized proof and a description in the form of answers to a standard questionnaire. The 17 systems presented are HOL, Mizar, PVS, Coq, Otter/Ivy, Isabelle/Isar, Alfa/Agda, ACL2, PhoX, IMPS, Metamath, Theorema, Leog, Nuprl, Omega, B method, and Minlog.

Reviews

From the reviews:

"The central idea of the book is to provide a comparison–somehow on the surface–of different proof systems. … the book is accessible to everybody with elementary school knowledge of mathematics. … this book is a must for everybody developing a proof system. … Everybody who uses (or like to use) a theorem prover will find it useful. … it is essential to locate your prover in the world of theorem proving." (Reinhard Kahle, Studia Logica, Vol. 87, 2007)

Editors and Affiliations

  • Institute for Computing and Information Sciences, Radboud University Nijmegen, Nijmegen, The Netherlands

    Freek Wiedijk

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation