Answer Set Programming (ASP) is a programming methodology designed for solving combinatorial search problems, where the goal is to find a solution among a finite but very large number of possibilities. Such problems are common in science and technology. In safety-critical applications of ASP it is important to have a higher level of confidence in the correctness of software than can be achieved by merely applying it to many test cases; mathematical methods must be used to prove with complete certainty that the program finds the correct answer in every possible case. This project develops such mathematical methods.
In the early days of ASP, the input languages of answer set solvers had a simple semantics based on the concept of a stable model. But many constructs added over the years to the language of ASP because programmers found them useful cannot be explained in terms of stable models in the sense of the original definition of that concept or its straightforward generalizations. Manuals written by the designers of answer set solvers explain the meaning of these programming constructs using examples and informal comments that appeal to the user's intuition, without references to any precise semantics. The first goal of this project is to characterize the semantics of ASP in a mathematically precise way using an extension of stable models to logical formulas with infinite conjunctions and disjunctions. Second, this semantics is used for verifying the correctness of ASP programs and optimization methods. The broader impacts of this work include collaboration with other research groups for dissemination, validation and adoption of the research results, and integration of the research into graduate education.
