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.

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

Standardization across multiple formulas in the entailment #31

Closed
melvic-ybanez opened this issue Oct 19, 2024 · 1 comment
Closed

Standardization across multiple formulas in the entailment #31

melvic-ybanez opened this issue Oct 19, 2024 · 1 comment
Assignees

Comments

@melvic-ybanez
Copy link
Owner

melvic-ybanez commented Oct 19, 2024

Right now, standardization is only applied to each formula separately. This can result to issues such as the one (partly) resolved by introducing Skolem suffixes. This is explained in detail in this release: https://github.com/melvic-ybanez/lohika/releases/tag/v0.2.1.

While the idea of Skolem suffixes can fix the issue with generated functions and constants, nothing is stopping the user from creating their own, with names that also have those suffixes. So, in rare(?) circumstances, a name clash can still occur.

The better way to fix this issue for good is to standardized everything in the entailment.

For now, we can only discourage users from naming constants and functions with Skolem suffixes, at least until this ticket is closed.

@melvic-ybanez melvic-ybanez self-assigned this Oct 25, 2024
@melvic-ybanez
Copy link
Owner Author

Closed by 002248e, 27d74c0, and 9f08f34

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

No branches or pull requests

1 participant