Open
Conversation
- remove SubEqDualAxiom, since redundant - simplify clauses using equality resolution with deletion - remove redundant clauses
This commit refactors the theory axioms for natural numbers, so that they are included not only if -tha is set to on, but also for -tha some. It is motivated by the idea that we sometimes want to exclude expensive integer-theory axioms (by setting -tha to some). In that case, we still want to include all theory axioms for natural numbers, since they are much more likely than integer axioms to contribute to a proof in the setting of Rapid.
Allows simplification of clauses: t=t+1 or C => C, where t is an arbitrary term.
…and s(0) This hack is motivated by the observation that there is no example known which is only provable using one of these terms.
Had to - adapt Inference::Rule to InferenceRule - use different naming for some theory axiom - manually redo the shift of createISE from MainLoop to SaturationAlgorithm
- turn off the lemma literal option -lls by default - add a new option -csd (off by default) to control the deletion inference rule for successor terms
|
Rapid-specific changes:
|
Contributor
|
@mina1604 - are these features still used with the state-of-the-art in Rapid? If so let's work together to get them merged, or at least updated with mainline Vampire. If not, let's close this. |
|
Yes they are - especially the first and last point (without lemmaless reasoning) |
Contributor
|
Leaving as-is until August 2023 as requested. :-) |
Contributor
|
@MichaelRawson: Let me know if you need some further input / context on the commits of this branch |
Contributor
Contributor
|
@mina1604 - now that the dust has settled on your doctorate (congratulations!), what do we want to do with this? Happy to do reasonable work to get it merged if it's still useful. |
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
5 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.
To ensure that Rapid support is maintained going forward we should merge the Rapid specific features into the master branch. This is just creating the initial pull request. The next step will be to merge master in, fix any issues, and then review the new features.