Re: [isabelle] Sledgehammer option to stop if first prover finds a proof



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 :

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






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