Skip to content

[issue1240] Keep axioms stratifiable in normalization edge case - #308

Open
grucla wants to merge 11 commits into
aibasel:mainfrom
grucla:issue1240
Open

[issue1240] Keep axioms stratifiable in normalization edge case#308
grucla wants to merge 11 commits into
aibasel:mainfrom
grucla:issue1240

Conversation

@grucla

@grucla grucla commented Aug 5, 2026

Copy link
Copy Markdown
Contributor

The normalization of the translator makes the axioms of a task unstratifiable if they contain an axiom that mentions its head predicate, possibly recursively, in its body under the scope of a universal quantifier. We fix this by using a different universal quantifier elimination for such axioms.

@grucla

grucla commented Aug 20, 2026

Copy link
Copy Markdown
Contributor Author

I ran some experiments where the output of the translator unexpectedly changed on some domains although they are no such edge cases. The names of some variables introduced by the translator change in output.sas. This is avoidable but would make the code less clear which is why I did not implement it. See my comment on the issue tracker (issue1240) for details.

@grucla
grucla marked this pull request as ready for review August 20, 2026 12:51
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.

1 participant