Email Gateway (Aug 18 2022 at 19:59): Email Gateway (Aug 18 2022 at 19:59):From: gottfried.barrow@gmx.com
This comment falls under the "Dude, this is awesome" category, and no
reply is needed. I try to keep my comments to a minimum, but I make this
one.
Bibliographies leading to bibliographies led me to Blanchett's
"Automatic Proofs and Refutations for Higher-Order Logic"
<http://www4.in.tum.de/%7Eblanchet/>.
There are developers of other provers who listen in, so this comment
could also serve as a feature request from one user, me, for their products.
I've said that I don't care about automatic proving. For my purposes,
whatever I prove I have to understand, so automatic proving doesn't help
me unless I can be shown the automatic prover's proof, and understand
the details, or have a general idea of what the prover did. My intended
audience, by and large, also won't be impressed by automatic proofs.
There has to be educational content in the details of my proofs, where
the amount of detail has to be balanced (which, of course, requires some
auto proving), but where there isn't a total absence of details.
On the other hand, as to counterexamples, there's no requirement that I
understand anything other than that the counterexample has proven me
wrong, so I'll be keeping in mind the Isabelle tools that will look for
counterexamples. As Blanchett says,
Novices and experts alike can enter invalid formulas and find
themselves wasting hours
(or days) on an impossible proof; once they identify and correct
the error, the proof is often easy.
I saw in the past a little of the results of Quickcheck, but I had
forgotten about the counterexample tools.
But back to automatic proving, I'm sure it'll come in handy when I have
"The Important Promising Conjecture", or even under less important
circumstances. What I think I don't want, I sometimes do want.
Power is whatever you need. I had a mini-debate with someone who had no
sympathy with the idea that I needed a proof assistant instead of an
automatic prover. Power to him was automatic proving. Power to me was
being able to specify the proof steps. I guess both are powerful, since
both take a massive amount of work to implement.
--GB
Last updated: Apr 25 2024 at 01:08 UTC