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 omega-completeness theorem for the many-sorted logic of here-and-there.

PDF

In Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning, 2023.

@inproceedings{omega23, title={Omega-Completeness of the Logic of Here-and-There and Strong Equivalence of Logic Programs}, author={Jorge Fandinno and Vladimir Lifschitz}, booktitle={Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning}, month={ }, url="http://www.cs.utexas.edu/users/ai-labpub-view.php?PubID=128008", year={2023} }