4 ms·
Yes, Coq has a tactics language. So does Isabelle. What I have in mind are primarily "Hammers", i.e. hooking in fully automatic theorem prover (e.g. MizAR for
by Cladode 7y ago
Yes, Coq has a
tactics language. So does Isabelle. What I have in mind are primarily
"Hammers", i.e. hooking in fully automatic theorem prover (e.g. MizAR for
Mizar, Sledgehammer for Isabelle/HOL, HOL(y)Hammer for HOL Light and
HOL4). As far as I'm aware, CoqHammer for Coq is
work-in-progress and does not yet provide the level of automation that you get from Sledgehammer in Isabelle/HOL for years. But admittedly, it's been 4-5 years since I last
used Coq. At the time, two core issues were the following:
- Existing automatic theorem provers often produced non-constructive
proofs.
- Existing automatic theorem provers are mostly for FOL, so the gap to
the much more powerful logics of Curry-Howard based provers is
bigger than with weaker systems.
Have both problems been solved comprehensively as of January 2020?
- logicchains 7y agoThey have not been solved. My point was that automation via Coq's tactic language can serve as a decent substitute for "push-button" automation like Hammers, at least if one's continually working in the same domain and so can build up a library of tactics.