ComparisonWithOtherSystems
There are a number of automatic theorems provers, proof assistants and math formalization systems. Some of them:
For a more complete list see Freek Wiedijk's list of Computer Math Systems.
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
HOL Light is a proof assistant in the HOL family. It is being used in the FlyspeckProject to machine-check Hales's proof of the Kepler conjecture.
Freek Wiedijk has described an encoding of the HOL Light logic into Coq: see [http://www.cs.ru.nl/~freek/notes/holl2coq.pdf]. Unfortunately, the overall approach is very inefficient.
Hol4 and ProofPower are said to have the same foundation as HOL light; if so, the same encoding should apply. Isabelle/HOL is also a system in the HOL family, and the foundational differences with HOL light should be minor.
The Mizar system (ignoring the default axioms which are based on Tarski/Grothendieck set theory, a strenghtening of ZFC) is based on unsorteed FOL. Encoding this logical system into Coq is straightforward.
- Caduceus http://why.lri.fr/caduceus/index.en.html
- Krakatoa http://krakatoa.lri.fr/
- Why http://why.lri.fr/index.en.html
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 PlanetMath 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.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.