Re: [isabelle] Isabelle2013-2-RC3 ATP e_par acid test



Am 05.12.2013 um 14:59 schrieb Makarius <makarius at sketis.net>:

> On Wed, 4 Dec 2013, Gottfried Barrow wrote:
> 
>> The short story is that I can reliably get non-terminating processes (or processes that can't be shut down, and that will run for a long time), but so far, I can only do that with the ATP e_par, and when it's started with a bunch of other ATPs.
> 
> This is the first time I learn about the existence of e_par.  It seems to be an add-on script to E prover by Josef Urban.  Maybe Jasmin can say something about the degree of supportedness within the Sledgehammer suite.
> 
> My general impression is that there are many experimental add-ons that are not widely used nor tested on the usual platforms.

Yes, "e_par" should be considered experimental. Beyond the technical issues, it didn't perform well on our benchmarks.

Jasmin





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