Use Vampire to resolve almost all unknown implications (without proof) #206
Conversation
This file contains 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
|
Wow, 7999 remaining is far better than I expected! (And is this excluding equivalences?) I'll merge for now due to the outstanding interest, but do consider adding a chapter to the blueprint describing the methodology and results. |
Command-Master
added a commit
to Command-Master/equational_theories
that referenced
this pull request
Oct 3, 2024
Merged
lyphyser
pushed a commit
to lyphyser/equational_theories
that referenced
this pull request
Oct 3, 2024
* Revert teorth#206 * Revert
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Use the Vampire ATP to prove/disprove many implications, transitively resolving almost all implications.
More work is needed to produce Lean proofs for the results, which are currently marked
conjecture. After this, the statistics are:explicit_proof_true: 23109
implicit_proof_true: 5295922
explicit_conjecture_true: 38949
implicit_conjecture_true: 1223057
unknown: 7999
implicit_conjecture_false: 1540725
explicit_conjecture_false: 79635
implicit_proof_false: 12994633
explicit_proof_false: 829607