Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

FINITE MAGMA EXPLORER: Use the finite magma graph rather than the general magma graph to detect new refutations #855

Closed
teorth opened this issue Nov 19, 2024 · 4 comments · Fixed by #856
Closed

FINITE MAGMA EXPLORER: Use the finite magma graph rather than the general magma graph to detect new refutations #855

teorth opened this issue Nov 19, 2024 · 4 comments · Fixed by #856
Assignees
@vlad902

Comments

@teorth
Copy link
Owner

teorth commented Nov 19, 2024

Pointed out in https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Austin.20pairs/near/483160464
@teorth teorth converted this from a draft issue Nov 19, 2024
@vlad902
Copy link
Contributor

vlad902 commented Nov 19, 2024

I think this may be as easy as using --finite-only with lake exe extract_implications unknowns in the CI workflow, but I'm not very familiar with FME so someone should double check me.

@vlad902
Copy link
Contributor

vlad902 commented Nov 19, 2024

Actually, took a quick look, that seems right.

@vlad902
Copy link
Contributor

vlad902 commented Nov 19, 2024

claim

@teorth teorth moved this from Unclaimed Outstanding Tasks to Claimed Tasks in Equational Theories Project Nov 19, 2024
vlad902 added a commit to vlad902/equational_theories that referenced this issue Nov 19, 2024
@vlad902
FME: Report finite magmas as new even if they're solved in the genera…
53c2b38 
…l graph (teorth#855)
@vlad902
Copy link
Contributor

vlad902 commented Nov 19, 2024

propose PR #856

@github-actions github-actions bot mentioned this issue Nov 19, 2024
Merged
@teorth teorth moved this from Claimed Tasks to In Progress in Equational Theories Project Nov 19, 2024
@github-project-automation github-project-automation bot moved this from In Progress to Completed Tasks in Equational Theories Project Nov 19, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@vlad902 vlad902

Labels
None yet
Projects
Equational Theories Project
Status: Completed Tasks
Milestone
No milestone
2 participants
@teorth @vlad902