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

Support second mini-gringo dialect and tau* variant with absolute value and modified division #15

Open
ZachJHansen opened this issue Aug 9, 2023 · 0 comments
Open

Support second mini-gringo dialect and tau* variant with absolute value and modified division #15

ZachJHansen opened this issue Aug 9, 2023 · 0 comments
Labels
A-syntax-tree Area: Abstract syntax tree A-translating Area: Language translations (like tau_star, ...) C-feature-requested Category: Requested feature E-hard Experience: Hard P-low Priority: Low

Comments

@ZachJHansen
Copy link
Collaborator

Clingo's definition of division/modulo differs from mathematical definition presented in "Verifying Tight Logic Programs with ANTHEM and VAMPIRE" in the case of negative divisors (uses truncation to zero instead of floor).

Up-to-date definitions are in Jorge & Vladimir's "Omega-Completeness..." draft, which adds absolute value as a function to mini-GRINGO and the two-sorted target language.

So do we want to make anthem clingo-compliant and add this?
omega.pdf
@teiesti teiesti added E-hard Experience: Hard C-bug Category: Bug A-syntax-tree Area: Abstract syntax tree A-translating Area: Language translations (like tau_star, ...) labels Sep 19, 2023
@ZachJHansen ZachJHansen added P-low Priority: Low C-feature-requested Category: Requested feature and removed C-bug Category: Bug labels Dec 8, 2023
@ZachJHansen ZachJHansen changed the title Add absolute value to resolve error in val_t(Z) definitions from "Verifying Tight..."? Support second mini-gringo dialect and tau* variant with absolute value and modified division Dec 8, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
A-syntax-tree Area: Abstract syntax tree A-translating Area: Language translations (like tau_star, ...) C-feature-requested Category: Requested feature E-hard Experience: Hard P-low Priority: Low
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@teiesti @ZachJHansen