Amazon cover image
Image from Amazon.com

The seventeen provers of the world / foreword by Dana S. Scott ; Freek Wiedijk (ed.).

Contributor(s): Material type: TextTextPublisher number: 11542384Series: Lecture notes in computer science ; 3600. | Lecture notes in computer science. Lecture notes in artificial intelligence. | Lecture notes in computer science. Lecture notes in artificial intelligence. AI systems.Publication details: Berlin ; New York : Springer, ©2006.Description: 1 online resource (xvi, 157 pages) : illustrationsContent type:
  • text
Media type:
  • computer
Carrier type:
  • online resource
ISBN:
  • 9783540328889
  • 3540328882
  • 3540307044
  • 9783540307044
Subject(s): Genre/Form: Additional physical formats: Print version:: Seventeen provers of the world.DDC classification:
  • 511.3/6 22
LOC classification:
  • QA155.7.E4 S48 2006eb
Other classification:
  • 31.10
  • 54.72
  • O141. 2-37
  • SS 4800
  • 510
  • DAT 706f
  • MAT 109f
Online resources:
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 [and others] -- B method / Dominique Cansell -- Minlog / Helmut Schwichtenberg.
In: OhioLINK electronic book center In: SpringerLinkReview: "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
Holdings
Item type Current library Collection Call number Status Date due Barcode Item holds
eBook eBook e-Library eBook LNCS Available
Total holds: 0

Includes bibliographical references and index.

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 [and others] -- 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

Print version record.

Available to OhioLINK libraries.

Powered by Koha