do not consider {inequality,general} splitting as naming a formula

[MichaelRawson]

Should fix #509 - the problem was that I over-eagerly removed stuff from congruence axioms with ep=RSTC. Mea culpa etc, I have eaten my humble pie twice now.

This one is quite subtle. The argument for skipping introduced symbols goes that you could do equality proxy completely before clausification, on the input problem - so you don't need to include introduced names because they aren't in the original problem. However we don't actually do equality proxy before clausification, and inequality splitting happens before equality proxy, changing the "input problem" in such a way that we need to include its definition predicates. I'm not sure about general splitting, but perhaps a similar problem exists so I've also included them just to be sure.

There are, I think, two solutions. This one - include congruence axioms for stuff we're not 100% sure about. Or, perhaps better - do the equality-proxy transform before clausification.

[easychair]

If clausification introduces new symbols, we cannot do EP before clausification. A

…

On Fri, 8 Dec 2023 at 10:37, Michael Rawson ***@***.***> wrote: Should fix #509 <#509> - the problem was that I over-eagerly removed stuff from congruence axioms with ep=RSTC. Mea culpa etc, I have eaten my humble pie twice now. This one is quite subtle. The argument for skipping introduced symbols goes that you could do equality proxy completely before clausification, on the input problem - so you don't need to include introduced names because they aren't in the original problem. *However* we don't actually do equality proxy before clausification, and inequality splitting happens before equality proxy, changing the "input problem" in such a way that we need to include its definition predicates. I'm not sure about general splitting, but perhaps a similar problem exists so I've also included them just to be sure. There are, I think, two solutions. This one - include congruence axioms for stuff we're not 100% sure about. Or, perhaps better - do the equality-proxy transform before clausification. ------------------------------ You can view, comment on, or merge this pull request online at: #510 Commit Summary - 6b5c0f7 <6b5c0f7> do not consider {inequality,general} splitting as naming a formula File Changes (3 files <https://github.com/vprover/vampire/pull/510/files>) - *M* Kernel/Signature.hpp <https://github.com/vprover/vampire/pull/510/files#diff-19f3cbbfd997d9cd880457089072bb20d51f589f9d7b51f817b7f1aaa7e92ae4> (2) - *M* Shell/GeneralSplitting.cpp <https://github.com/vprover/vampire/pull/510/files#diff-00d850e8e0690c07c287039996c93c6c29e39362a2b0fe8ad80a731b4f9e5362> (2) - *M* Shell/InequalitySplitting.cpp <https://github.com/vprover/vampire/pull/510/files#diff-dfa188f0b59d12892272b58d4948c83a3ccf17afa8c0d205122a4ec075df0876> (4) Patch Links: - https://github.com/vprover/vampire/pull/510.patch - https://github.com/vprover/vampire/pull/510.diff — Reply to this email directly, view it on GitHub <#510>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABVY4BLZ67TIRAH5HJQY3BDYILUXBAVCNFSM6AAAAABAMOVDI2VHI2DSMVQWIX3LMV43ASLTON2WKOZSGAZTENBQGY3DSOI> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[MichaelRawson]

If clausification introduces new symbols, we cannot do EP before clausification.

New equations we have to watch out for. New symbols can be fine; for instance, it's OK to skip Skolems.

Anyhow, @quickbeam123 prefers the manually-marked solution, closing.