do not axiomatise congruence for introduced symbols

[MichaelRawson]

Equality proxy with -ep RSTC adds congruence axioms for functions and predicates in the signature, with the exception of answer literals and the equality proxy predicate itself.

As far as I can tell it could skip introduced symbols altogether, because one could imagine performing the equality-proxy transformation before clausification.

[quickbeam123]

1. Do we know exactly which symbols this is meant to affect? (Beyond Skolems, I guess...)
2. Why the condition "the equality proxy predicate" - wasn't that take care of until now?

[MichaelRawson]

1. If markIntroduced() is used as intended (and I think it is), then essentially any symbol that isn't in the problem.
2. It was! Currently we ignore answer literals and the equality (proxy) predicate, after this change we ignore all introduced symbols.

[quickbeam123]

Ad 2. Yes, stupid me. I was reading the diff in the wrong direction ;)

Ad 1. But have you gone through all the sites where we possibly create a symbol marked introduced to check that omitting ep-congruence for it would be OK?

I think it's not a correct approach (unless we mark ep=RSTC as incomplete), e.g., for any symbol introduction which relies on symbol definitions via =. For instance, twee_goal_transformation, function_definition_introduction, and some types of fool_elimination ...

[MichaelRawson]

Ad 1. But have you gone through all the sites where we possibly create a symbol marked introduced to check that omitting ep-congruence for it would be OK?

I did the first part of this - all the sites mark their symbols as introduced - but failed to do the second part where I check it was actually OK. Sorry!

I think it's not a correct approach (unless we mark ep=RSTC as incomplete), e.g., for any symbol introduction which relies on symbol definitions via =. For instance, twee_goal_transformation, function_definition_introduction, and some types of fool_elimination ...

You're right, some of these don't work - I guess because they introduce equations or rely on preserving equational satisfiability? So I think (and will patch the code if you agree) that we can at least skip Skolems and predicate definitions, by an equisatisfiability argument.

[quickbeam123]

You're right, some of these don't work - I guess because they introduce equations or rely on preserving equational satisfiability?

I think it's simpler than that. It's just because if a transformation relies on adding an equational element (like a definition), the "swap argument" (i.e., "ep first, this only later") suddenly does not work - since "this done later" would reintroduce equalities to a problem where they got initially eliminated by ep.

So I think (and will patch the code if you agree) that we can at least skip Skolems and predicate definitions, by an equisatisfiability argument.

I think it's a much better idea to play this game on a "let's list the good guys"-basis, rather than "let's assume all introduced works". Also because of future coders reaching after an innocuous function like addFreshFunction not having to worry wether this will work under some exotic ep=RSTC :)

[quickbeam123]

Still, I think some non-trivial testing will be in order!

[MichaelRawson]

I think it's simpler than that. It's just because if a transformation relies on adding an equational element (like a definition), the "swap argument" (i.e., "ep first, this only later") suddenly does not work - since "this done later" would reintroduce equalities to a problem where they got initially eliminated by ep.

True. One could imagine hacking these transformations to use the proxy predicate instead, but then I'm not sure what the right condition to preserve satisfiability would be.

I think it's a much better idea to play this game on a "let's list the good guys"-basis, rather than "let's assume all introduced works". Also because of future coders reaching after an innocuous function like addFreshFunction not having to worry wether this will work under some exotic ep=RSTC :)

Agreed! I'll do it for Skolems and naming then. :-)

[MichaelRawson]

Fixed. How do you want to test?

[quickbeam123]

How do you want to test?

Exhaustively ;)

[quickbeam123]

Done, by the way. No weird saturations occurred.

If -ep RSTC was a powerful trick (it kind of was, for instgen ;)) this would be a cool improvement! About 100 problems more solved, on average, across TPTP FOF.

By the way, there is one problem getting robustly penalized for this:
./vampire_rel_michael-skip-introduced-for-ep_6869 -sa discount -awr 10 -ep RSTC Problems/SEU/SEU359+1.p
Master will solve it much faster thanks to a shortcut in the proof via a congruence for a arity-3 naming predicate.

I think it's ready to go!

[MichaelRawson]

Thank you for testing!

If -ep RSTC was a powerful trick (it kind of was, for instgen ;)) this would be a cool improvement! About 100 problems more solved, on average, across TPTP FOF.

I guess the next round of Snaking will pick up if it becomes useful for strategy schedules - and we can resurrect InstGen if you suspect it would be useful.