Re: [isabelle] Fwd: Sledgehammer all subgoals?



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

> On 23 Sep 2015, at 11:34, Tom Ridge via Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk> wrote:
> 
> (resend, after sending from wrong email address)
> 
> On 15 September 2015 at 11:34, Larry Paulson <lp15 at cam.ac.uk> wrote:
> 
>> On 15 Sep 2015, at 11:05, Tom Ridge <tom.j.ridge at 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
>> 
>> 
>> 
>> 





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