search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
282 stars 49 forks source link

set kbo weights of fool constants to 1 no matter the weight scheme #559

Closed quickbeam123 closed 3 months ago

quickbeam123 commented 3 months ago

Fixes https://github.com/vprover/vampire/issues/557

joe-hauns commented 3 months ago

Why/in which rule do we need the property that $false is least? Can we just make saturation incomplete when the fool constant weight is not 1 and the respective options are enabled?

quickbeam123 commented 3 months ago

In FOOL paramodulation, I believe. Feel free to check https://github.com/vprover/vampire/issues/557 and https://arxiv.org/pdf/1510.04821

What you suggest is also a possibility...

joe-hauns commented 3 months ago

I see. I missed the crutial option -foolp... I think we still need to make the saturation incomplete if a user sets _foolConstant to something different to 1 using the weight setting file, right?

mezpusz commented 3 months ago

I was thinking that in the future, we could just prepend the built-in precedences in front of the precedence vector, but I see this is not possible because of e.g. numeral constants which we don't know the number of in advance. Anyways, I approve of this solution, I'm just a bit worried that we have similar interdependencies elsewhere which we don't yet know of.

quickbeam123 commented 3 months ago

I tried not to follow the path for making _foolConstant settable from a file, but maybe it's possible somehow?

In any case, I think the file input is so rare that working on a robust way of figuring out completeness for user-specified weight scheme and precedence might not be worth the effort. Unless it's already there and a one-liner would fix it?