Skip to content

Turn on ROBOT's equivalent_pair check - #23

Open
hoodcm wants to merge 4 commits into
mainfrom
robot-equivalent-pair
Open

hoodcm wants to merge 4 commits into
mainfrom
robot-equivalent-pair

Conversation

@hoodcm

@hoodcm hoodcm commented Oct 1, 2026 •

Copy link
Copy Markdown
Collaborator

Part of #5.

Check Data checked Why
equivalent_pair Logical axioms Two named classes aren't declared equivalent.

ROBOT's standard check, at ERROR. Nothing on main fails it, so no data changes. All tests pass.

@jclerman

jclerman commented Oct 1, 2026

Copy link
Copy Markdown
Collaborator

Nice. However, I'd enable this at ERROR. Any reason not to? WARN won't be visible unless people are manually checking, and I don't think we intend to have any logically-duplicate classes.

@jclerman

Copy link
Copy Markdown
Collaborator

NOTE we should also run this after reasoning.

@jclerman
jclerman force-pushed the robot-equivalent-pair branch from 905eed7 to f40e1f0 Compare October 12, 2026 23:04
@jclerman
jclerman self-requested a review October 12, 2026 23:04
@hoodcm

hoodcm commented Oct 12, 2026

Copy link
Copy Markdown
Collaborator Author

Raised to ERROR.

On running it after reasoning: the robot reason step in CI already runs with --equivalent-classes-allowed asserted-only, which fails on any equivalence the reasoner infers. This check covers the asserted ones, so together they cover both.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants