3 ms·
I have not used Sledgehammer but even with a SAT solver we still need to handle quantifier instantiations. And in case the SAT solver fails (I mean time-outs, n
by fspeech 4y ago
I have not used Sledgehammer but even with a SAT solver we still need to handle quantifier instantiations. And in case the SAT solver fails (I mean time-outs, not finding counter-examples) we won't get clues on how to fix it. SAT solvers work on CNF, which is very far from the deeply structured formulaes that math tends to generate.
- mbrodersen 4y agoI am not a working mathematician and don’t care about formalising mathematics. For the things I do care about (proving code correct) tools like Sledgehammer are awesome.