In answer set programming, a program verication task can be sometimes accomplished by transforming rules into first-order sentences so that the task is reduced to reasoning in classical logic, and invoking a resolution theorem prover. The proof assistant anthem, which implements this idea, allows us to reason about programs written in mini-gringo--a subset of the input language of the grounder gringo. The goal of this paper is to extend the syntax of terms permitted in that subset. First, instead of the specific choice of arithmetic functions made in earlier publications on mini-gringo, we approach integer arithmetic in an abstract way, so that different choices are allowed for different dialects of the language. Second, symbolic constants can be used now as function symbols. This generalization preserves the main property of the more limited form of the language established in earlier work: mini-gringo rules can be faithfully represented by first-order sentences.

PDF

To Appear In Proceedings of the European Conference on Logics in Artificial Intelligence, 2025.

@inproceedings{lif25, title={Generalizing the Syntax of Terms in Mini-gringo}, author={Vladimir Lifschitz}, booktitle={Proceedings of the European Conference on Logics in Artificial Intelligence}, month={ }, url="http://www.cs.utexas.edu/users/ai-labpub-view.php?PubID=128126", year={2025} }