Rhodes, Greece. September 2-8, 2023.
Copyright © 2023 International Joint Conferences on Artificial Intelligence Organization
Theory of strongly equivalent transformations is an essential part of the methodology of representing knowledge in answer set programming. Strong equivalence of two programs can be sometimes characterized as the possibility of deriving the rules of each program from the rules of the other in some deductive system. This paper describes a system with this property for the language mini-GRINGO. The key to the proof is an ω-completeness theorem for the many-sorted logic of here-and-there.