6 ms·
> The counterexample generator is very powerful because it leverages the knowledge base of the theorem prover (all the accumulated lemmas, etc.) among other thi
by hnipps 6mo ago
> The counterexample generator is very powerful because it leverages the knowledge base of the theorem prover (all the accumulated lemmas, etc.) among other things.
That's a really interesting application. Could be very powerful for what I'm doing. Thank you!
- derrak 6mo agoHappy to help. In general, I think counterexample generation is more important than proofs when it comes to software (most of our software is “trivially” wrong). The world might not be ready for full-blown formal verification, but I think it is ready for formal specification and counterexample generation.