3 ms·
> You can also get the theorem prover itself to hang or crash; if you work with theorem provers often, you'll even do this unintentionally, many times! Proving
by nickdrozd 3y ago
> You can also get the theorem prover itself to hang or crash; if you work with theorem provers often, you'll even do this unintentionally, many times!
Proving something false is a grave sin for a prover. On the other hand, failing to prove something true is not only forgivable, but inevitable as per the incompleteness theorem. While ideally this failure would presented in terms of a nice error message, crashes are preferable to unsoundness. Crashes can even be deliberately induced as a defensive measure: https://hal.science/hal-04096390/document https://hal.science/hal-04096390/document
- CHY872 3y agoIt really depends on how automated the prover is, this is kind of like reinforcement learning optimising something unintentionally. Theorem prover bugs are problematic if relied upon, but most of the bugs folks cite are only usable in very strange circumstances, and most practitioners will not see their results invalidated by such a bug. E.g. iirc falso required a type with more than 256 variants. If you don’t have one of those, it won’t affect you! Essentially, you fix the bug, re-run your hol or whatever, and hope your theorem is still true. Obviously this only applies to bugs in the implementation as opposed to an unsound logic.
- IIAOPSW 3y agoI feel like getting stuck in an infinite loop is a more appropriate encoding of "undecidable"