All4x4Tables: Integrate straggler counterexamples #324
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
Expands the number of finite magmas in All4x4Tables by gathering a couple of finite magmas which were previously used in counterexamples elsewhere. Benefits: * For all these examples, each satisfied and refuted equation was determined, which settled 236 previously unknown anti-implications. * These examples were put through the proof planner, meaning that while the number of magmas increased greatly (from 543 to 740) the number of checks the kernel has to perform remains about the same. New sources: * Magmas constructed by the Z3 solver gathered from teorth#308. * Magmas constructed by the Vampire theorem prover gathered from teorth#276. * A 5x5 magma manually constructed by Pace Nielsen. Unknowns now at 21679.
With the importation of the straggler examples, the Vampire Disproofs become unnecessary. This commit removes the disproofs, and changes the documentation with explanations about how Vampire disproofs can be generated. It also updates the blueprint with more sources of counterexamples. The unknowns remain at 21679.
Updates the implication database used for transitive closure pruning in `All4x4Tables`. This time it does not result in further reductions in the number of checks.
|
Great, thanks! By the way, another finite magma by Pace was proposed recently in https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/visualization.20of.20graph.20closure |
|
How did you produce the lists of which implications each table proves? I'm running Vampire with more time per equality, so I want to add the magmas it finds directly to here |
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.
Expands the number of finite magmas in All4x4Tables by integrating a couple of finite magmas which were previously used in counterexamples elsewhere.
Benefits:
which settled 236 previously unknown anti-implications.
number of magmas serving as counterexamples increased greatly (from 543 to 740) the number of checks the
kernel has to perform remains about the same. The
generate_lean.pyscript canalso prune them using transitive closure whenever new implications are proven.
The newly added sources:
With the importation of the straggler examples, the current set of Vampire disproofs become redundant, so these are removed. The commit changes the VampireProven documentation with a bit of explanation about how Vampire
Disproof*.leanfiles will appear when Vampire disproofs are generated. It also updates the blueprint with more sources of counterexamples.Unknowns at 21679.