Ordered Completion for Non-Locally Tight mini-gringo Programs
Jan Heuer
TL;DR
This work develops a rigorous framework for capturing the stable-model semantics of arbitrary mini-gringo programs through ordered completion, addressing the limitations of standard completion for non-tight and non-locally-tight programs. It introduces well-supported models as a semantic bridge and extends ordered completion to mini-gringo, including a level-mapping variant to accommodate infinite stable models. The approach is implemented in the Anthem verification tool, enabling first-order verification of program properties and external-specifications for non-tight ASPs, with practical demonstrations on simple examples. The results provide a basis for verifying external equivalence and formal specifications in ASP, while also outlining current limitations and directions for future enhancements, such as implementing level mapping and integrating higher-order reasoning.
Abstract
Completion is a well-known transformation that captures the stable model semantics of logic programs by turning a program into a set of first-order definitions. Stable models are models of the completion, but not all models of the completion are stable models. For tight programs (programs without positive recursion) the two semantics coincide. Recently this correspondence was extended to locally tight programs, which avoid non-terminating recursion. However, unlike tightness, local tightness cannot be checked with simple syntactic methods. Completion is crucial for verifying answer set programs, especially for external equivalence: a form of equivalence based on selected output predicates under certain inputs. Standard equivalence and adherence to a first-order specification are special cases of external equivalence. The anthem verification tool has two limitations for checking external equivalence: (1) there is no way to check local tightness automatically, and (2) it is not possible to verify programs that are not locally tight. Therefore, alternatives to completion are of interest. This thesis investigates ordered completion, introduced in [Asuncion et al., 2012], which captures stable models of arbitrary logic programs, but only for finite models. This work extends ordered completion to the mini-gringo language (a subset of the language used by the clingo solver). Additionally, it introduces a modification of ordered completion to handle infinite stable models. This extended ordered completion is implemented in anthem as a translation, and initial experiments demonstrate its use for verifying simple logic programs.