The Seventeen Provers of the World [electronic resource] :Foreword by Dana S. Scott / edited by Freek Wiedijk.
by Wiedijk, Freek [editor.]; SpringerLink (Online service).
Material type:
BookSeries: Lecture Notes in Computer Science: 3600Publisher: Berlin, Heidelberg : Springer Berlin Heidelberg, 2006.Description: XVI, 159 p. Also available online. online resource.ISBN: 9783540328889.Subject(s): Computer science | Software engineering | Artificial intelligence | Computer Science | Artificial Intelligence (incl. Robotics) | Software Engineering | Mathematical Logic and Formal LanguagesDDC classification: 006.3 Online resources: Click here to access online | Item type | Current location | Call number | Status | Date due | Barcode |
|---|---|---|---|---|---|
| TJ210.2-211.495 (Browse shelf) | Available | ||||
| Long Loan | MAIN LIBRARY | Q334-342 (Browse shelf) | Available |
Browsing MAIN LIBRARY Shelves Close shelf browser
| TA329-348 Advances in Verification of Time Petri Nets and Timed Automata | R-RZ Structure of Enteric Neurons | HF54.5-54.56 Managing Dynamic Networks | Q334-342 The Seventeen Provers of the World | QA273.A1-274.9 The Random-Cluster Model | TA1-2040 Excavations and Foundations in Soft Soils | QC19.2-20.85 Group Theory |
Informal -- HOL -- Mizar -- PVS -- Coq -- Otter/Ivy -- Isabelle/Isar -- Alfa/Agda -- ACL2 -- PhoX -- IMPS -- Metamath -- Theorema -- Lego -- Nuprl -- ?mega -- B Method -- Minlog.
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.
There are no comments for this item.