3 ms·
How does being classical help with automation? I'm more familiar with ACL2, which seems to gain a lot more on the automation front from being first-order than f
by kd0amg 7y ago
How does being classical help with automation? I'm more familiar with ACL2, which seems to gain a lot more on the automation front from being first-order than from anything else (though it has sort of a weird take on the excluded middle).
- Cladode 7y agoThat's a subtle and deep question. One example are nominal techniques. Consider Nominal Isabelle. It is known that nominal techniques are contructive. However, when adding nominal techniques to a classical logic, it is natural to express some of this using double negation, leading to only a small blowup in formula size. Existing proof automation can easily handle this blowuip. Doing the same in a simple minded constructive way, leads to a massive formula size increase, defeating (at the time) existing proof automation. This was a while back, maybe the problem has been solved now, I have not followed this field. But as far as I'm aware, the 'hammering' approach to proof automation that has been working well with Isabelle/HOL has been successfully ported to Coq/Agda etc.