ComparisonWithOtherSystems

page was renamed from ComparisionWithOtherSystems

There are a number of automatic theorems provers, proof assistants and math formalization systems. Some of them:

• http://www.cs.utexas.edu/users/moore/acl2/acl2-doc.html
• http://ghilbert.org
• http://www.qedeq.org/index.html
• http://www.cl.cam.ac.uk/users/jrh/hol-light/
• http://isabelle.in.tum.de/index.html
• http://au.metamath.org/index.html
• http://www.mizar.org
• ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/index.html
• http://www.cs.cornell.edu/Info/Projects/NuPrl/
• http://planetmath.org
• http://www.lemma-one.com/ProofPower/index/

For a more complete list see http://www.cs.ru.nl/~freek/digimath/index.html.

It would be nice to give brief list of their advantages and disadvantages compared to Coq.

• Kam, Robert C., "Case Studies in Proof Checking" available from http://www.cs.sjsu.edu/faculty/beeson/Masters/KamThesis.pdf includes a critique of Coq and a comparison with the Mizar system. ** Among other things, it is claimed that Coq's abstract foundations introduce incompatibilities between foundational libraries and make it hard to reuse existing theories. The non-trivialness of type-casting compounds this problem. See LibraryIncompatibility

=== Related Tools for Software Verification ===

• Caduceus http://why.lri.fr/caduceus/index.en.html
• Krakatoa http://krakatoa.lri.fr/
• Why http://why.lri.fr/index.en.html

=== Why you should choose Coq ===

It's free. Coq is licensed under LGPL, so it's much easier to modify it and develop it. For example, although Mizar has very large theorems collection, there is no prover source available.

It's strict. Comparing Coq to wiki-based systems like http://planetmath.org shows it's that Coq is much nicer organized. Although it's easy to contribute to wiki system, it's hard to manage them. It's hard to trust just wiki.