[isabelle] The usefulness of smt (and simp)

I was getting annoyed at Sledgehammer because it seemed I was setting it up with the right theorems, but it wasn't being successful.

That led me to adding theorems to "simp" and running "by simp" before Sledgehammer, which I had heard rumors about, but some things you have to learn on your own, which demonstrates the usefulness of hearing or reading things for future use.

Also, I had been staying away from smt because of the talk I'd seen about problems with the AFP.

However, some algorithms are just good for doing things that others can't do.

I attach a screen shot at 29Kbytes. No metis proof can be found for the particular situation, but a good smt proof comes to the rescue. Only occasionally do the ATPs resort to smt proofs, but when the ATPs need to, they seem to do it at the right time.

If I say good things about tools like smt, then maybe certain developers will keep doing good things to help it help me.


Attachment: 120211_sfS_smt_proof.png
Description: PNG image

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