RI: Small: Mathematical Analysis of an Answer Set Programming Language

答案集编程（ASP）是一种设计用于解决组合搜索问题的编程方法，其目标是在有限但非常大量的可能性中找到解决方案。 这样的问题在科学和技术领域很常见。 在ASP的安全关键应用程序中，重要的是要对软件的正确性有更高的信心，而不仅仅是将其应用于许多测试用例;必须使用数学方法来完全确定地证明程序在每种可能的情况下都能找到正确的答案。 在ASP的早期，答案集求解器的输入语言具有基于稳定模型概念的简单语义。 但是，多年来添加到ASP语言中的许多结构，因为程序员发现它们很有用，不能在该概念的原始定义或其简单概括的意义上用稳定模型来解释。 由答案集求解器的设计者编写的手册使用示例和非正式的评论来解释这些编程结构的含义，这些评论吸引了用户的直觉，而没有引用任何精确的语义。 这个项目的第一个目标是在一个数学上精确的方式使用扩展的稳定模型的逻辑公式与无限的合取和析取ASP的语义特征。 其次，将该语义用于验证ASP程序和优化方法的正确性。 这项工作的更广泛的影响包括与其他研究小组的合作，传播，验证和采用的研究成果，并将研究纳入研究生教育。

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.