Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] metis -unused theorems

view this post on Zulip Email Gateway (Aug 22 2022 at 18:02):

From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear Isabelle users,

I have the following question which is not an actual problem, but I am
just wondering
why metis behaves this way:

the following keeps happening:
sledgehammer gives one (or more) proof(s) by metis,
but when I apply the suggested proof, I get the output message "unused
theorems"

(When this happens afterwards either I delete the named unused theorems,
or use
(some of) them to help sledgehammer to give me another simpler proof.)

I just find this metis behaviour a bit puzzling -any insight?

Thanks a lot,
Best wishes,
Angeliki

view this post on Zulip Email Gateway (Aug 22 2022 at 18:02):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Angeliki,

It is hard to tell without a concrete example, but a possible explanation is that Sledgehammer includes a minimization phase, described in e.g. Section 6.6.5 of my thesis:

https://mediatum.ub.tum.de/doc/1097834/1097834.pdf <https://mediatum.ub.tum.de/doc/1097834/1097834.pdf>

However, since proof search in FOL is not a decision procedure, we have to use a time limit when invoking the prover for minimizing. Hence as a result, we lose any guarantees that the minimized result is minimal.

In the file src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML, on line 129, you will find this constant:

val slack_msecs = 200

You could try increasing it to, e.g., 2000 and see if it has an impact. There's of course a tradeoff between fast minimization and "minimal" minimization. It seems like it's hard to get both.

Cheers,

Jasmin

view this post on Zulip Email Gateway (Aug 22 2022 at 18:03):

From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear Jasmin,

thanks a lot for your answer.

view this post on Zulip Email Gateway (Aug 22 2022 at 18:03):

From: Christian Sternagel <c.sternagel@gmail.com>
Dear Angeliki,

just an experience report.

I regularly encounter these "unused theorems" warnings you are talking
about.

However, I would not blindly remove such unused theorems, since in my
experience it is often the case that the corresponding metis proof will
be quite a bit slower after that.

cheers

chris

view this post on Zulip Email Gateway (Aug 22 2022 at 18:04):

From: Dominique Unruh <unruh@ut.ee>
Hi,

However, I would not blindly remove such unused theorems, since in my

Last updated: Nov 21 2024 at 12:39 UTC