Email Gateway (Aug 19 2022 at 10:06): Email Gateway (Aug 19 2022 at 10:06):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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.
Regards,
GB
120211_sfS_smt_proof.png
Last updated: Apr 25 2024 at 04:18 UTC