非分层逻辑程序稳态模型的存在性

本文提出了一个与Answer Set编程和规划相关的基本结果。自稳态模型语义定义以来，首次给出了稳态模型存在的逻辑程序类别的语法特征描述。这一条件在定义新的用于检查一致性和计算答案集的算法，以及改进现有系统方面可能具有实际意义。本文的方法是引入一种新型标准形式（任何逻辑程序都可归约至该标准形式），将注意力集中于循环依赖。随后以标准形式下的程序（标准程序）给出技术结果，且不影响一般性。该结果基于识别程序中的循环，表明整个程序的稳态模型由对应于这些循环的适当子程序的稳态模型组成，并定义了循环图（Cycle Graph）。该图的每个顶点对应一个循环，每个边对应一个把手（handle），即一个包含同时出现于两个循环中的原子的文字，实际上决定了它们之间的连接。事实上，把手在其所在循环中作为规则头出现时，其真值，对其在体中出现的循环（们）的原子的真值具有决定性影响。因此，我们可以引入把手路径的概念，将不同循环连接起来。如果对于每个奇数循环我们都能找到具有某些属性的把手路径，则保证稳态模型的存在。