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 >> _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
