Formal methods for answer set programming

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).