Hi,
Tobias asked me to look at Sledgehammer and see if it would be
possible to improve the relevance filter and the proof reconstruction
to get a better success rate. As a first step towards that, I was
thinking of refactoring the Sledgehammer code. In particular:
1. Put all the
On Wed, 13 Jan 2010, Jasmin Blanchette wrote:
Tobias asked me to look at Sledgehammer and see if it would be possible
to improve the relevance filter and the proof reconstruction to get a
better success rate. As a first step towards that, I was thinking of
refactoring the Sledgehammer
Hi Makarius,
Am 13.01.2010 um 17:57 schrieb Makarius:
The ATP manager is relatively new (and clean),
I have to disagree here -- but not with the new part. I find it
dubious that ATP_Manager is based on ATP_Wrapper and not the other way
around. As a result, adding a new ATP (besides E,
PS Since I suggested to Jasmin to work on s/h, I obviously welcome his
initiative. It is important that we have one person who has the time and
the responsibility, just like other people feel responsible for fun etc.
Tobias
Jasmin Blanchette wrote:
Hi Makarius,
Am 13.01.2010 um 17:57 schrieb
On Wed, 13 Jan 2010, Tobias Nipkow wrote:
PS Since I suggested to Jasmin to work on s/h, I obviously welcome his
initiative. It is important that we have one person who has the time and
the responsibility, just like other people feel responsible for fun
etc.
Yes, responsibility is the key
