[isabelle-dev] Coral and Sledgehammer

[Tobias Nipkow]

I rarely feel the need for answer literals, i.e. to let provers
synthesize terms for me. And I doubt it would often work (although in
that paper they do benefit from it). Given that Sledgehammer is not a
trivial piece of engineering, I would not want to burden it with more
"proactive" functionality (unless it is easy to add), esp if none of the
ATPs support it.

Tobias

Lawrence Paulson schrieb:
> Thanks for reminding me of this paper. It states that the modified version of SPASS implements answer literals, which would allow sledgehammer for the first time to handle variables in subgoals. This could be quite useful. What do others think?
> 
> Of course, we would also have to consider the extent to which this modified version is supported. It doesn't look like they have added answer literals to the latest version of SPASS.
> Larry
> 
> On 20 Nov 2010, at 23:55, John Matthews wrote:
> 
>> Hi Larry, Tobias,
>>
>> Are either of you familiar with this JAR article about Coral, by Graham Steel and Alan Bundy?
>>
>>  http://www.lsv.ens-cachan.fr/~steel/publis.php?onlykey=SB-jar06
>>
>> I've only skimmed the paper, but in Section 3.1 (page 4) it talks about a modified version of Spass that can be used to refute first-order inductive conjectures. Apparently the underlying algorithm can also be used to prove these conjectures (when it terminates), but it's unclear whether the extended Spass can be used for that.
>>
>> At any rate, I was thinking it might be useful for someone to extend Sledgehammer to call these Spass extensions. Even just getting counterexamples back from failed conjectures could be very nice.
>>
>> -john
>>