Table of Contents

Informal / Henk Barendregt.
HOL / John Harrison, Konrad Slind, Rob Arthan.
Mizar / Andrzej Trybulec.
PVS / Bart Jacobs, John Rushby.
Coq / Laurent Théry, Pierre Letouzey, Georges Gonthier.
Otter/Ivy / Michael Beeson, William McCune.
Isabelle/Isar / Markus Wenzel, Larry Paulson.
Alfa/Agda / Thierry Coquand.
ACL2 / Ruben Gamboa.
PhoX / Christophe Raffalli, Paul Rozière.
IMPS / William Farmer.
Metamath / Norman Megill.
Theorema / Wolfgang Windsteiger, Bruno Buchberger, Markus Rosenkranz.
Lego / Conor McBride.
Nupri / Paul Jackson.
Omega / Christoph Benzmüller ... [et al.].
B method / Dominique Cansell.
Minlog / Helmut Schwichtenberg. "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."--Jacket.
Image
OPEN
eu03.alma.exlibrisgroup.com
"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."--Jacket.
Wiedijk, Freek
-
Springer
2006
9783540307044
RefWorks