Otter/Ivy

Abstract. We compare the styles of several proof assistants for mathematics. We present Pythagoras’ proof of the irrationality of √ 2 both informal and formalized in (1) HOL, (2) Mizar, (3) PVS, (4) Coq, (5) Otter/Ivy, (6) Isabelle/Isar, (7) Alfa/Agda, (8) ACL2, (9) PhoX, (10) IMPS, (11) Metamath, (12) Theorema, (13) Lego, (14) Nuprl, (15) Ωmega, (16) B method, (17) Minlog. proof assistant author of proof page informal Henk Barendregt 17 1 HOL John Harrison, Konrad Slind, Rob Arthan 18 2 Mizar Andrzej Trybulec 27 3 PVS Bart Jacobs, John Rushby 31 4 Coq Laurent Th´ery, Pierre Letouzey, Georges Gonthier 35 5 Otter/Ivy Michael Beeson, William McCune 44 6 Isabelle/Isar Markus Wenzel, Larry Paulson 49 7 Alfa/Agda Thierry Coquand 58 8 ACL2 Ruben Gamboa 63 9 PhoX Christophe Raffalli, Paul Rozi`ere 76 10 IMPS William Farmer 82 11 Metamath Norman Megill 98 12 Theorema Wolfgang Windsteiger, Bruno Buchberger, Markus Rozenkranz 106 13 Lego Conor McBride 118 14 Nuprl Paul Jackson 127 15 Ω...

• Type: Conference
• Year: 2006
• Where: TPHOL
• Authors: Michael Beeson, William McCune
• Keywords: Artificial Intelligence, Proof Assistant, Proof Assistant Author, PVS Bart Jacobs, TPHOL 2006