Email Gateway (Aug 22 2022 at 16:43): Email Gateway (Aug 22 2022 at 16:43):From: Peter Lammich <lammich@in.tum.de>
Hi,
is there an option that stops the other provers if sledgehammer finds a
proof.
Use-case:
I have several subgoals, and want to see which of them are (easily)
provable. So, currently, I invoke sledgehammer in parallel on all
subgoals:
subgoal sledgehammer sorry
subgoal sledgehammer sorry
...
subgoal sledgehammer sorry
In order to make this effeicient, the sledgehammer tool should stop if
it has found and reconstructed SOME proof, to give its resources to the
remaining sledgehammers.
Of course, a sledgehammer-all-subgoals command would be even better.
Best,
Peter
Email Gateway (Aug 22 2022 at 16:45):From: Frédéric Tuong <ftuong@vt.edu>
Hi Peter,
I have finally implemented the "sledgehammer-all-subgoals" command here:
https://github.com/ssrg-vt/isabelle_para/releases/tag/Isabelle2017_sledgehammer_all
The new commands are "sledgehammer_first" which stops in front of a
first answer, and "sledgehammer_all" which performs the execution of a
list of
[sledgehammer_first;
sledgehammer_first;
...
sledgehammer_first]
depending on the number of first subgoals given as argument.
As example, the following lemma is comparing the different versions of
sledgehammer:
lemma assumes A B C D E
shows "A ∧ B ∧ C ∧ D ∧ E ∧ F"
apply (intro conjI)
sledgehammer
sledgehammer_first
sledgehammer_all ⇌ 4 ― ‹TODO: show the full reconstruction proof
whenever @{command sledgehammer_all}
succeeds on all subgoals.›
sledgehammer_all ⇌ 6
oops
Cheers,
Frédéric
Thu, 8 Feb 2018 13:16:50 -0500, Peter Lammich :
Email Gateway (Aug 22 2022 at 16:45):From: Peter Lammich <lammich@in.tum.de>
Hi,
thank you very much.
But do I really need to fork the Isabelle repository for that?
@Jasmin: Can this be pushed to main Isabelle?
Last updated: Apr 26 2024 at 20:16 UTC