Sort out FOOL paramodulation and Cases[Simp]#861
Open
mezpusz wants to merge 8 commits into
Open
Conversation
…r FOOLParamodulation
MichaelRawson
approved these changes
Jun 5, 2026
| "Sets between three ways of dealing with the FOOL exhaustiveness axiom X0 = $true | X0 = $false:\n" | ||
| "(1) axiom: adds the axiom,\n" | ||
| "(2) generating: uses FOOL paramodulation as a generating inference rule,\n" | ||
| "(3) simplifying: a simplifying variant of the FOOL paramodulation inference rule."; |
Contributor
There was a problem hiding this comment.
Would "off" be a reasonable value here?
Contributor
Author
There was a problem hiding this comment.
We are hiding all this behind the hasFOOL()==true condition, but of course, we could also consider disabling it completely. I honestly cannot tell which one makes more sense, what's you opinion?
Contributor
There was a problem hiding this comment.
That seems fine - what I was thinking about is the case where we do have FOOL, but we don't need to do any reasoning about terms being Boolean. This may not actually happen in practice, of course.
| resLits->push( curr != lit | ||
| ? curr | ||
| : EqHelper::replace(curr, t, troo)); | ||
| resLits->push(EqHelper::replace(curr, TermList(t), replaceWithTroo ? troo : fols)); |
Contributor
There was a problem hiding this comment.
Would it be cleaner to pass the value of replaceWithTroo ? troo : fols directly to this function? Fairly minor though so nbd.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
There is an axiomatization and multiple inferences for handling Booleans, and they are kind of a mess. The goal of the present PR is uniformize the inferences, so that we can decide later which ones are still useful. My suggestion would be to eventually remove
FOOLParamodulation, but we can also probably very easily implement it inCases(basically taking the first result instead of all). In particular, the following changes are included:hasBoolVar()==truein thePropertyobject, which in turn toggles some additional inferences like primitive instantiation. Due to this, now with the missing (but unnecessary axiom) we seemingly lose some problems when Cases is turned on.Detailed comparisons with master are to follow.
Cases FOL:
Discount master 10254 (0) vs branch 10260 (6)
Otter master 10354 (0) vs branch 10361 (7)
Cases HOL Discount:
master unsat: 2235 (13) sat: 1 (0) cputime: 8817.91 s instructions: 44196749 Mi memory: 118099.22 MB
branch unsat: 2231 (9) sat: 14 (13) cputime: 8820.62 s instructions: 43948531 Mi memory: 118149.41 MB
Cases HOL Otter:
master unsat: 2202 (20) sat: 1 (0) cputime: 9240.33 s instructions: 44841767 Mi memory: 141257.77 MB
branch unsat: 2200 (18) sat: 14 (13) cputime: 9239.07 s instructions: 44603251 Mi memory: 143950.84 MB
FOOLP HOL Discount:
master unsat: 2200 (37) sat: 14 (0) cputime: 8513.03 s instructions: 42983868 Mi memory: 118078.84 MB
branch unsat: 2183 (20) sat: 14 (0) cputime: 8735.23 s instructions: 43785102 Mi memory: 118122.17 MB
FOOLP HOL Otter:
master unsat: 2163 (28) sat: 14 (0) cputime: 8878.40 s instructions: 43640601 Mi memory: 144348.84 MB
branch unsat: 2151 (16) sat: 14 (0) cputime: 9175.95 s instructions: 44560333 Mi memory: 143307.99 MB