[Matryoshka-devel] Evil axioms

Stephan Schulz schulz at eprover.org
Thu Apr 20 16:38:48 CEST 2017

Hi Jasmin!

> On 20. Apr 2017, at 15:53, Blanchette, J.C. <j.c.blanchette at vu.nl> wrote:
> Hi all,
> Thanks for your input! This is very useful. I'll just answer all emails in one go, focusing on those things where I have more to say than "Yes, thanks for the links" or "Good idea" or "OK". I've printed a few papers already.
> Josef wrote:
>> Larry had some manual blacklisting in SH long ago.
> Indeed, we still have some of it, but it's mostly historical. His blacklisting used to be necessary because of the unsound encoding.
> Pascal wrote:
>> Probably very empirical at first.  A project for a bachelor student?
> Indeed. The empirical flavor doesn't exactly excite me about doing it, but a well-done empirical study can be very illuminating once it's done. There's no hurry, but we can keep this in the back of our minds for veriT. Even though there's a priori no HO in it, it's very relevant to the "hammer"-style of proving and hence to Matryoshka's goals, and also surely to Josef's AI4REASON and Cezary's SMART projects.

I’ve always had the feeling that the presence if certain axioms, or sets of axioms,
has a major influence on search behaviour. I don’t know if simple blacklisting is
a good approach, but Waldmeister did e.g. recognise theories and use the presence
or absence as features for strategy selection, and also for computing term orderings
that work well with these axiomatisations.



------------------------------ It can be done! ---------------------------------
          Please email me as schulz at eprover.org (Stephan Schulz)

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 204 bytes
Desc: Message signed with OpenPGP
URL: <http://lists.gforge.inria.fr/pipermail/matryoshka-devel/attachments/20170420/7466d3ca/attachment.sig>

More information about the matryoshka-devel mailing list