Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben

2006 | Buch

Introduction Kapitel lesen Erstes Kapitel lesen

The Seventeen Provers of the World

Foreword by Dana S. Scott

herausgegeben von: Freek Wiedijk

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

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.

Inhaltsverzeichnis

Frontmatter
Introduction
Abstract
Some years ago during lunch, Henk Barendregt told me about a book (Algorithmics by David Harel) that compared programming languages by showing the same little program in each language that was treated. Then I thought: I could do that for proof assistants! And so I mailed various people in the proof assistant community and started the collection that is now in front of you.
Freek Wiedijk
Informal
Abstract
Statement
\(\sqrt{2} \in \mathbb{Q}\)
Definitions
Definition of P
Definition on ℕ the predicate
\(P(m) \Leftrightarrow \exists n \cdot m^2 = 2n^2 \& m > 0\).
Henk Barendregt
HOL
Abstract
Statement
~rational(sqrt(&2))
Definitions
Definition of sqrt
let root = new_definition
’root(n) x = @u. (&0 < x = = > &0 < u) / u pow n = x’;;
let sqrt = new_definition
’sqrt(x) = root(2) x’;;
John Harrison, Konrad Slind, Rob Arthan
Mizar
Abstract
Statement
sqrt 2 is irrational
Andrzej Trybulec
PVS
Abstract
In particular the definition of sqrt below comes from this library. Answers by John Rushby.
Statement
NOT Rational?(sqrt(2))
Bart Jacobs, John Rushby
Coq
Abstract
Statement
irrational (sqrt 2%nat).
Laurent Théry, Pierre Letouzey, Georges Gonthier
Otter/Ivy
Abstract
Statement
m(a,a) = m(2,m(b,b))
Michael Beeson, William McCune
Isabelle/Isar
Abstract
Statement
\(sqrt~ (real (2::nat))\not\in \mathbb{Q}\)
Markus Wenzel, Larry Paulson
Alfa/Agda
Abstract
Statement
prime p → noether A (multiple p) → isNotSquare p
Thierry Coquand
ACL2
Abstract
Statement
(implies (equal (* x x) 2) (and (realp x) (not (rationalp x))))
Ruben Gamboa
PhoX
Abstract
Statement
/ m,n : N (m^ N2 = N2 * n^ N2 -> m = N0 & n = N0)
Christophe Raffalli, Paul Rozière
IMPS
Abstract
Statement
not #(sqrt(2),qq)
William Farmer
Metamath
Abstract
Statement
$p |- ( sqr ’ 2 ) e/ QQ
Norman Megill
Theorema
Abstract
Statement
Theorem[”gsqrt[2] irrational”, ¬ rat[\(\sqrt{2}\)]]
Wolfgang Windsteiger, Bruno Buchberger, Markus Rozenkranz
Lego
Abstract
Statement
{b|nat}{a|nat}(Eq (times two (times a a)) (times b b))-> (Eq a zero / Eq b zero)
Conor McBride
Nuprl
Abstract
Statement
¬(∃u:ℚ. u * q u = 2 / 1)
Paul Jackson
Ωmega
Abstract
Statement
(not (rat (sqrt 2)))
Christoph Benzmüller, Armin Fiedler, Andreas Meier, Martin Pollet, Jörg Siekmann
B Method
Abstract
Statement
!(n,m).(n:NATURAL& m:NATURAL => (n*n=2*(m*m)<=>(n=0&m=0)))
Dominique Cansell
Minlog
Abstract
Statement
all x,p,q.2===x*x -> x===p#q -> F
Helmut Schwichtenberg
Backmatter
Metadaten
Titel
The Seventeen Provers of the World
herausgegeben von
Freek Wiedijk
Copyright-Jahr
2006
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-540-32888-9
Print ISBN
978-3-540-30704-4
DOI
https://doi.org/10.1007/11542384

Premium Partner

    Bildnachweise