[isabelle] Automation is awesome; one bibliography leads to another



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.