9 ms·
Although Coq is using constructive logic by default, it is not limited to it. One can use classical logic results just by importing the "Classical" module. Or c
by yaantc 10y ago
Although Coq is using constructive logic by default, it is not limited to it. One can use classical logic results just by importing the "Classical" module. Or course one then loose the benefits of having a constructive proof (like code extraction), but if the interest is only in checking a mathematical proof then it can be acceptable. The choice and trade-off is up to the user.
- mafribe 10y agoThat is true, but does proof automation work as well for classical reasoning in Coq as it does in Isabelle/HOL where classical reasoning is 'baked in' from the start? As far as I'm aware, the question of moving the "sledgehammer" approach to a constructive setting is still an open problem.