[isabelle-dev] Coral and Sledgehammer

[Lawrence Paulson]

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
>