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

RI：小：答案集编程语言的数学分析

• 批准号: 1422455
• 负责人: Vladimir Lifschitz
• 金额: $ 40.4万
• 依托单位: University of Texas at Austin
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-07-01 至 2018-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1422455&HistoricalAwards=false
• 关键词: RI; Small; Mathematical; Analysis; Answer

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.

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