The Seventeen Provers of the World
This page is the home of a comparison between proof assistants by having a proof of the irrationality of the square root of two in seventeen different proof assistants. There is also something like a consumer test of these systems.
Here are the source files of those proofs:
- HOL Light by John Harrison: hol.ml hol_alt.ml; HOL4 by Konrad Slindt: hol4.ml; ProofPower by Rob Arthan: proofpower.ml
- Mizar by Andrzej Trybulec: mizar.miz
- PVS by Bart Jacobs and John Rushby: pvs.dmp
- Coq by Laurent Théry: coq.v coq_letouzey.v coq_gonthier.v; Matita by Andrea Asperti: matita.ma
- Otter/Ivy by Michael Beeson and William McCune: otter.in otter.out ivy.in ivy.out
- Isabelle/Isar by Markus Wenzel: isar.thy; script style by Larry Paulson: isabelle.thy; Isabelle/ZF by Larry Paulson: isabelle_ZF.thy
- Alfa/Agda by Thierry Coquand: agda.alfa
- ACL2 by David Russinoff: acl2.lisp acl2.out; ACL2(r) by Ruben Gamboa: acl2r.event acl2r.out
- PhoX by Christophe Raffalli and Paul Rozière: phox.phx
- IMPS by William Farmer: imps.t
- Metamath by Norman Megill: metamath.mm
- Theorema by Wolfgang Windsteiger, Bruno Buchberger, Markus Rosenkranz: theorema.nb theorema_notRatSqrt2.nb theorema_coprime.nb
- Lego by Conor McBride: lego.l
- Nuprl by Paul Jackson: nuprl.thy nuprl.prl
- Omega, by Christoph Benzmüller, Armin Fiedler, Andreas Meier and Martin Pollet: omega.rpy omega.pds
- B method, by Dominique Cansell: b.mch b.arc
- Minlog, by Helmut Schwichtenberg: minlog.scm minlog_unary.scm
Some of these files are now a few years old: they might not work with the latest version of the corresponding system.
(last modification 2007-02-27)
|