02673nam 2200553 a 450 991048458480332120200520144314.03-540-32888-210.1007/11542384(CKB)1000000000232728(SSID)ssj0000320029(PQKBManifestationID)11235193(PQKBTitleCode)TC0000320029(PQKBWorkID)10342767(PQKB)11468301(DE-He213)978-3-540-32888-9(MiAaPQ)EBC3067630(PPN)12312977X(EXLCZ)99100000000023272820051223d2006 uy 0engurnn|008mamaatxtccrThe seventeen provers of the world /foreword by Dana S. Scott ; Freek Wiedijk (ed.)1st ed. 2006.Berlin ;New York Springerc20061 online resource (XVI, 162 p.) Lecture notes in computer science. Lecture notes in artificial intelligence,0302-9743 ;3600Bibliographic Level Mode of Issuance: Monograph3-540-30704-4 Includes bibliographical references and index.Informal -- HOL -- Mizar -- PVS -- Coq -- Otter/Ivy -- Isabelle/Isar -- Alfa/Agda -- ACL2 -- PhoX -- IMPS -- Metamath -- Theorema -- Lego -- Nuprl -- ?mega -- B Method -- Minlog.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.Lecture notes in computer science.Lecture notes in artificial intelligence ;3600.Proof theoryData processingAlgebraComputer programsProof theoryData processing.AlgebraComputer programs.511.3/6Wiedijk Freek1961-1740262MiAaPQMiAaPQMiAaPQBOOK9910484584803321The seventeen provers of the world4197514UNINA