Modular Answer Set Programming as a Formal Specification Language
Modular Answer Set Programming as a Formal Specification Language
复制标题
DOI：
10.1017/s1471068420000265
复制
发表时间：
2020-08
影响因子：
1.4
通讯作者：
Pedro Cabalar;Jorge Fandinno;Yuliya Lierler
中科院分区：
文献类型：
--
作者：
Pedro Cabalar;Jorge Fandinno;Yuliya Lierler
本文研究了回答集程序设计（ASP）的形式化验证问题，即给出一个形式化证明，证明给定（非基础）逻辑程序P的回答集与P编码的问题的解正确对应，而不管问题实例如何。为了这个目的，我们使用一个正式的规范语言的基础上ASP模块，使每个模块可以被证明捕捉到一些非正式方面的问题，在一个孤立的方式。这种规范语言依赖于一个新的定义（可能是嵌套的，一阶）程序模块，可以将本地隐藏的原子在不同的级别。然后，对逻辑程序P进行验证，相当于证明了P与其模块规格说明之间的某种等价性。
Abstract 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.