[Matryoshka-devel] Evil axioms

Blanchette, J.C. j.c.blanchette at vu.nl
Fri Apr 21 17:01:19 CEST 2017

Hi Stephan, Martin,

Stephan wrote:

> 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.

That's interesting!

Martin wrote:

> 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).



[*] https://people.mpi-inf.mpg.de/~jblanche/itp2012-spass.pdf

More information about the matryoshka-devel mailing list