[Matryoshka-devel] Evil axioms
j.c.blanchette at vu.nl
Fri Apr 21 17:01:19 CEST 2017
Hi Stephan, Martin,
> 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,
Simple blacklisting is extremely crude, and we're going away from that. A more flexible mechanism to down-prioritize the axioms, as described in e.g. Section 5 of "More SPASS with Isabelle" [*], could be useful here. (For E, we proceed more indirectly, by playing with the weights, as you might recall.)
> 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.
> In particular, the law of excluded middle, Leibniz equality and
> extensionality are cut-strong. It's not exactly the kind of evil that
> you described, but it might come in handy at some point.
Thanks, that's good to know, e.g. as related work in a future "evil axioms" paper (if such an idea ever materialize, and if indeed single axioms can be found to be sufficiently evil).
More information about the matryoshka-devel