Email Gateway (Aug 22 2022 at 11:18): Email Gateway (Aug 22 2022 at 11:18):From: Tom Ridge via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
(resend, after sending from wrong email address)
On 15 September 2015 at 11:34, Larry Paulson <lp15@cam.ac.uk> wrote:
On 15 Sep 2015, at 11:05, Tom Ridge <tom.j.ridge@googlemail.com> wrote:
If it is not too much effort to add, this feature would be quite useful to
me (and to others?). Presumably the implementation is easy - conjunct-up
the goals and feed them to sledgehammer?This particular suggestion would not work. You would get nothing unless
all the goals could be solved, and forming the conjunction of two problems
is particularly damaging for resolution (to see why, consider the details
of the translation into clause form).
Do you really mean the approach won't work? Yes, if one of the goals cannot
be solved, you get nothing, but that is OK for my use case, and is one
possible interpretation of what "sledgehammer all goals" should mean (the
other being that those goals that can be solved, are solved, and the others
are untouched). Surely the approach of "conjuncting-up" is not worse than
invoking sledgehammer twice? (My expectation is that if there is shared
structure between the proofs, the performance might even be better.)
Can’t you identify the difficult case simply by looking at it? And
possibly the simp_all method could be of use here.
In this case, given the lack of this feature, I have indeed manually proved
the goals (by invoking various procedures several times). But I'm looking
for functionality that allows me to avoid doing this.
BTW happy birthday!
T
Larry Paulson
Email Gateway (Aug 22 2022 at 11:18):From: Larry Paulson <lp15@cam.ac.uk>
If the formula is converted to clause form using the traditional method of negation followed by conversion into CNF, then your idea would result in a geometric increase in the number of clauses. This is because the conjunctions would be transformed into disjunctions, which would have to be completely multiplied out.
It is conceivable that sledgehammer now uses a more sophisticated conversion method, but still you are making the problem much more difficult and would have to hope that much of the difficulty could be automatically detected and removed.
Larry
Email Gateway (Aug 22 2022 at 11:26):From: Tom Ridge via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear All,
Sorry for the easy question, but I couldn't find the answer in the
documentation.
How can I apply sledgehammer to solve all subgoals?
e.g.
lemma "True & True"
apply(rule)
At this point, if I click on the "Sledgehammer" tab in jedit and click
apply, it shows me a solution to the first goal. But I want it to solve all
the goals.
Thanks
Email Gateway (Aug 22 2022 at 11:26):From: Larry Paulson <lp15@cam.ac.uk>
I don't believe that such an option exists. Even with one goal, you are spawning up to 5 subprocesses on your machine. The idea anyway that you are trying to tackle a particularly tough problem, so it's natural to tackle them one at a time.
I wonder: is there much demand for this option?
Larry
Email Gateway (Aug 22 2022 at 11:26):From: Peter Lammich <lammich@in.tum.de>
On Di, 2015-09-15 at 10:11 +0100, Larry Paulson wrote:
I don't believe that such an option exists. Even with one goal, you are spawning up to 5 subprocesses on your machine. The idea anyway that you are trying to tackle a particularly tough problem, so it's natural to tackle them one at a time.
I wonder: is there much demand for this option?
Another use-case of sledgehammer is just to find the necessary theorems to
easily solve a goal. Sledgehammer will not find hard proofs itself, but
is very good at deducing proofs from theorems the user did not even know about.
Assuming sufficient computing power is available, a (auto-) sledgehammer
on all sub-goals in the background would imho be useful: Ideally, while
you are trying to prove the first sub-goal manually, sledgehammer
already solves the others for you.
Email Gateway (Aug 22 2022 at 11:26):From: Larry Paulson <lp15@cam.ac.uk>
This particular suggestion would not work. You would get nothing unless all the goals could be solved, and forming the conjunction of two problems is particularly damaging for resolution (to see why, consider the details of the translation into clause form).
Can’t you identify the difficult case simply by looking at it? And possibly the simp_all method could be of use here.
Larry Paulson
Last updated: May 06 2024 at 08:19 UTC