论文标题
模块化答案集编程作为正式规范语言
Modular Answer Set Programming as a Formal Specification Language
论文作者
论文摘要
在本文中，我们研究了答案集编程（ASP）的正式验证问题，即获得正式证明，表明给定（非地面）逻辑程序P的答案集正确地与P，无论问题实例如何，与P所编码的问题有关。为此，我们使用基于ASP模块的正式规范语言，以便可以证明每个模块以孤立的方式捕获问题的某些非正式方面。这种规范语言依赖于（可能嵌套的，一阶）程序模块的新颖定义，该定义可能包含不同级别的局部隐藏原子。然后，验证逻辑程序P量构成证明P与其模块化规范之间的某种等效性。正在考虑在TPLP中接受。
In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order) program modules that may incorporate local hidden atoms at different levels. Then, verifying the logic program P amounts to prove some kind of equivalence between P and its modular specification. Under consideration for acceptance in TPLP.
