Catálogo de publicaciones - libros
The Seventeen Provers of the World: Foreword by Dana S. Scott
Freek Wiedijk (eds.)
Resumen/Descripción – provisto por la editorial
No disponible.
Palabras clave – provistas por la editorial
Artificial Intelligence (incl. Robotics); Software Engineering; Mathematical Logic and Formal Languages
Disponibilidad
| Institución detectada | Año de publicación | Navegá | Descargá | Solicitá |
|---|---|---|---|---|
| No detectada | 2006 | SpringerLink |
Información
Tipo de recurso:
libros
ISBN impreso
978-3-540-30704-4
ISBN electrónico
978-3-540-32888-9
Editor responsable
Springer Nature
País de edición
Reino Unido
Fecha de publicación
2006
Información sobre derechos de publicación
© Springer-Verlag Berlin Heidelberg 2006
Tabla de contenidos
doi: 10.1007/11542384_1
Introduction
Freek Wiedijk
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.
Palabras clave: Prime Number; Mathematical Proof; Proof Assistant; Irreducible Element; Prime Number Theorem.
Pp. 1-9
doi: 10.1007/11542384_2
Informal
Henk Barendregt
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$ .
Pp. 10-10
doi: 10.1007/11542384_3
HOL
John Harrison; Konrad Slind; Rob Arthan
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’;;
Palabras clave: Inference Rule; High Order Logic; Logical Core; Jordan Curve Theorem; Primitive Rule.
Pp. 11-19
doi: 10.1007/11542384_4
Mizar
Andrzej Trybulec
Statement sqrt 2 is irrational
Palabras clave: Natural Deduction; Jordan Curve Theorem; Adjusted Version; Mizar Mathematical Library; Grammatical Analyzer.
Pp. 20-23
doi: 10.1007/11542384_5
PVS
Bart Jacobs; John Rushby
In particular the definition of sqrt below comes from this library. Answers by John Rushby. Statement NOT Rational?(sqrt(2))
Pp. 24-27
doi: 10.1007/11542384_6
Coq
Laurent Théry; Pierre Letouzey; Georges Gonthier
Statement irrational (sqrt 2%nat).
Palabras clave: Standard Library; Lambda Calculus; Inductive Construction; Proof Term; Interactive Theorem Prove.
Pp. 28-35
doi: 10.1007/11542384_7
Otter/Ivy
Michael Beeson; William McCune
Statement m(a,a) = m(2,m(b,b))
Pp. 36-40
doi: 10.1007/11542384_8
Isabelle/Isar
Markus Wenzel; Larry Paulson
Statement $sqrt~ (real (2::nat))\not\in \mathbb{Q}$
Palabras clave: Natural Deduction; Proof Assistant; Proof Script; Proof Tool; Isar Proof.
Pp. 41-49
doi: 10.1007/11542384_9
Alfa/Agda
Thierry Coquand
Statement prime p → noether A (multiple p) → isNotSquare p
Palabras clave: Localic Version; Formal Language; Type Theory; Case Notation; Actual Version.
Pp. 50-54
doi: 10.1007/11542384_10
ACL2
Ruben Gamboa
Statement (implies (equal (* x x) 2) (and (realp x) (not (rationalp x))))
Pp. 55-66