|
|
|
|
| LEADER |
02962cam a22005174a 4500 |
| 005 |
20140605114229.0 |
| 008 |
051223s2006 gw a b 001 0 eng |
| 010 |
|
|
|a 2005939043
|
| 020 |
|
|
|a 9783540307044 (softcover : alk. paper)
|
| 020 |
|
|
|a 3540307044 (softcover : alk. paper)
|
| 040 |
|
|
|a DLC
|c DLC
|b hrv
|d HR-ZaFER
|e ppiak
|
| 050 |
0 |
0 |
|a QA155.7.E4
|b S48 2006
|
| 082 |
0 |
0 |
|a 511.3/6
|2 22
|
| 245 |
0 |
4 |
|a The seventeen provers of the world /
|c foreword by Dana S. Scott ; Freek Wiedijk (ed.).
|
| 260 |
|
|
|a Berlin ;
|a New York :
|b Springer,
|c c2006.
|
| 300 |
|
|
|a xvi, 157 p. :
|b ill. ;
|c 24 cm.
|
| 490 |
0 |
|
|a Lecture notes in computer science,
|x 0302-9743 ;
|v 3600.
|a Lecture notes in artificial intelligence
|
| 504 |
|
|
|a Includes bibliographical references and index.
|
| 505 |
0 |
0 |
|t Introduction
Freek Wiedijk.
|t Informal
Henk Barendregt.
|t HOL
John Harrison, Konrad Slind, Rob Arthan.
|t Mizar
Andrzej Trybulec.
|t PVS
Bart Jacobs, John Rushby.
|t Coq
Laurent Thery, Pierre Letouzey, Georges Gonthier.
|t Otter/Ivy
Michael Beeson, William McCune.
|t Isabelle/Isar
Markus Wenzel, Larry Paulson.
|t Alfa/Agda
Thierry Conquad.
|t ACL2
Ruben Gamboa.
|t PhoX
Christophe Raffalli, Paul Roziere.
|t IMPS
William Farmer.
|t Metamath
Norman Megill
|t Theorema
Wolfgang Windsteiger, Bruno Buchberger, Markus Rozenkranz.
|t Lego
Conor McBride.
|t Nuprl
Paul Jackson.
|t Omega
Christoph Benzmueller, Armin Fiedler, Andreas Meier, Martin Pollet, Jorg Siekmann.
|t B Method
Dominique Cansell.
|t Minlog
Helmut Schwichtenberg.
|t Author Index.
|
| 506 |
0 |
|
|a Introduction --- Freek Wiedijk
|
| 506 |
0 |
|
|a Informal --- Henk Barendregt
|
| 506 |
0 |
|
|a HOL --- John Harrison, Konrad Slind, Rob Arthan
|
| 506 |
0 |
|
|a Mizar --- Andrzej Trybulec
|
| 506 |
0 |
|
|a PVS --- Bart Jacobs, John Rushby
|
| 506 |
0 |
|
|a Coq --- Laurent Théry, Pierre Letouzey, Georges Gonthier
|
| 506 |
0 |
|
|a Otter/Ivy --- Michael Beeson, William McCune
|
| 506 |
0 |
|
|a Isabelle/Isar --- Markus Wenzel, Larry Paulson
|
| 506 |
0 |
|
|a Alfa/Agda --- Thierry Coquand
|
| 506 |
0 |
|
|a ACL2 --- Ruben Gamboa
|
| 506 |
0 |
|
|a PhoX --- Christophe Raffalli, Paul Rozière
|
| 506 |
0 |
|
|a IMPS --- William Farmer
|
| 506 |
0 |
|
|a Metamath --- Norman Megill
|
| 506 |
0 |
|
|a Theorema --- Wolfgang Windsteiger, Bruno Buchberger, Markus Rozenkranz
|
| 506 |
0 |
|
|a Lego --- Conor McBride
|
| 506 |
0 |
|
|a Nuprl --- Paul Jackson
|
| 506 |
0 |
|
|a Ωmega --- Christoph Benzmüller, Armin Fiedler, Andreas Meier, Martin Pollet, Jörg Siekmann
|
| 506 |
0 |
|
|a B Method --- Dominique Cansell
|
| 506 |
0 |
|
|a Minlog --- Helmut Schwichtenberg
|
| 650 |
|
0 |
|a Proof theory
|c Data processing.
|
| 650 |
|
0 |
|a Algebra
|x Computer programs.
|
| 700 |
1 |
|
|a Wiedijk, Freek,
|d 1961-
|
| 856 |
4 |
2 |
|3 Publisher description
|u http://www.loc.gov/catdir/enhancements/fy0663/2005939043-d.html
|
| 906 |
|
|
|a 7
|b cbc
|c orignew
|d 2
|e epcn
|f 20
|g y-gencatlg
|
| 942 |
|
|
|2 udc
|c K
|
| 955 |
|
|
|a pc17 2005-12-23
|a jp00 2006-04-08
|a jp00 2006-04-24
|c jp43 2006-07-21 to subj
|a aa07 2006-09-12
|
| 999 |
|
|
|c 34771
|d 34771
|
