We would like to develop methods for verifying programs in the input language of the answer set solver clingo using software created for the automation of reasoning in first-order theories. As a step in this direction, we extend Clark’s completion to a class of clingo programs that contain arithmetic operations as well as intervals and prove that every stable model is a model of generalized completion. The translator anthem calculates the completion of a program and represents it in a format that can be processed by first-order theorem provers. Some properties of programs can be verified by anthem and the theorem prover vampire, working together.

PDF

In Fields of Logic and Computation III, Essays Dedicated to Yuri Gurevich on the Occasion of His 80th Birthday, pp. 190-209, 2020. Springer.

@incollection{yurifest, title={Towards Verifying Logic Programs in the Input Language of clingo}, author={Vladimir Lifschitz and Patrick Lühne and Torsten Schaub}, booktitle={Fields of Logic and Computation III, Essays Dedicated to Yuri Gurevich on the Occasion of His 80th Birthday}, month={ }, publisher={Springer}, pages={190-209}, url="http://www.cs.utexas.edu/users/ai-labpub-view.php?PubID=127803", year={2020} }