Answer set programming (ASP) is a declarative programming paradigm for the design and implementation of knowledge-intensive applications, particularly useful for modeling problems involving combinatorial search. The input languages of the first ASP software systems had the attractive property of a simple, fully specified declarative semantics, making it possible to use formal methods to analyze ASP programs – to verify correctness, for example, or to show that two programs were equivalent. Since that time, many useful new constructs have been added to input languages. The increase in usability, however, has come at the expense of a fully specified semantics, as the semantics of newer constructs has not quite kept pace with the most general syntax that solvers can handle. In this thesis, we will describe one approach to bridging the gap between mathematical formulations of the semantics of ASP languages and the current state of the languages themselves. Our approach is to view ASP programs as corresponding to infinitary formulas (formulas with infinitely long conjunctions and disjunctions). In addition to a semantics for ASP programs, we would like to have general methods for analyzing programs based on that semantics. For example, we would like to know when we are licensed to replace one rule with another within a program, without changing the meaning of the program. Answers to questions of this nature are based on the notion of “strong equivalence”, well-known in the ASP community. Intuitively, two rules are strongly equivalent if they are interchangeable in the context of any program. In this thesis, we will describe how this notion can be extended to infinitary formulas. We show that strong equivalence between such formulas can be established using an infinitary system of natural deduction, and in many cases in a finite deductive system. We give general methods for simplifying the translations of some common ASP constructs, and provide examples showing how our semantics and the formal methods we develop can be used to prove program correctness.

PDF

PhD Thesis, University of Texas at Austin. Doctoral Dissertation defended at the University of Texas.

@phdthesis{harrison:thesis, title={Formal Methods for Answer Set Programming}, author={Amelia Harrison}, month={ }, school={University of Texas at Austin}, note={Doctoral Dissertation defended at the University of Texas}, url="http://www.cs.utexas.edu/users/ai-labpub-view.php?PubID=127656", year={2017} }