最小逻辑程序与通用表格法在答案集编程中的应用

### 最小逻辑程序与通用表格法在答案集编程中的应用 #### 一、最小逻辑程序概述 在逻辑编程领域，生成与任意命题理论强等价的最小逻辑程序是一个重要的研究方向。我们考虑了两种生成最小逻辑程序的方法：一种是基于语法的方法，专注于规则和文字出现次数较少的程序；另一种是基于语义的方法，关注使用演绎强度尽可能大的规则的程序。 ##### 1. 示例程序 给出了几个示例程序： - $\Pi_1 = \{p ∨¬p, ¬p ∧¬q →⊥\}$ - $\Pi_2 = \{p ∨¬p, q →p\}$ - $\Pi_3 = \{p ∨¬p, ¬p →¬q\}$ - $\Pi_4 = \{p ∨¬p, ¬q ∨p\}$ 这些示例可用于与某些转换方法进行比较。例如，对理论 $\Gamma$ 应用特定转换后得到程序 $\Pi_2$ 以及额外规则 $\{p∨¬p∨¬q\}$，但该额外规则被 $\Pi_2$ 中的 $p∨¬p$ 所包含。 ##### 2. GPI 算法应用 GPI 算法在生成最小逻辑程序方面表现出色。以理论 $\{(¬p →q) →(¬p →r)\}$ 为例，之前的翻译得到六个规则：$\{(q ∧¬p →⊥), (q →¬r), (¬p →¬p), (¬p ∨¬r), (¬p →¬p ∨¬q), (¬p ∨¬q ∨¬r)\}$，去除重言式和被包含的规则后可简化为 $\{(q ∧¬p →⊥), (q →¬r), (¬p ∨¬r)\}$，但这并非最小程序。而 GPI 算法能得到强等价的最小程序 $\{(q ∧¬p →⊥), (¬p ∨¬r)\}$。此外，当有多种选择时，GPI 方法能获取所有可能的最小程序。 再看将不同知识源的程序片段组合的情况。若 $\Pi = \{(¬r ∧q →p), (¬p →r ∨s)\}$ 且 $\Pi' = \{(r →p), (¬r →q)\}$，这两个程序单独分析时都是最小的，且 $\Pi ∪\Pi'$ 中没有规则被其他规则包含。应用 GPI 算法后，得到唯一的最小强等价程序 $\{(¬r →p), (r →p), (¬r →q)\}$。 #### 二、蕴含关系与 s - 素蕴含项 在之前的示例中，尽管所有蕴含项都是素的，但有些蕴含项能蕴含其他蕴含项。这与经典情况不同，在 HT 逻辑中，语法上更简单并不意味着蕴含关系。例如，除了 1 - 之外的所有蕴含项都被 $\overline{2}\overline{0}$ 所蕴含。 ##### 1. s - 素蕴含项定义 我们引入了 s - 素蕴含项的概念。理论 $\Gamma$ 的蕴含项 $r$ 若不存在 $\Gamma$ 的蕴含项 $r'$ 使得 $r' |< r$，则称 $r$ 为语义素蕴含项（简称 s - 素蕴含项）。在示例中，唯一的 s - 素蕴含项是 1 - 和 $\overline{2}\overline{0}$。 ##### 2. 计算 s - 素蕴含项方法 由于包含关系意味着蕴含关系，计算 s - 素蕴含项可以作为之前 GPI 算法的后处理步骤，即移除一些非 s - 素的素蕴含项。另一种更高效的方法是对算法进行适当修改，从一开始就忽略被蕴含的蕴含项。 ##### 3. 规则蕴含与等价的句法特征 对于规则 $r$ 和基本规则 $r'$，$r |= r'$ 当且仅当满足以下条件： 1. $B^−_r ⊆B^−_{r'}$ 2. $Hd^−_r ⊆Hd^−_{r'} ∪B^+_{r'}$ 3. $B^+_r ⊆B^+_{r'} ∪Hd^−_{r'}$ 4. $Hd^+_r ⊆Hd^+_{r'} ∪B^−_{r'}$ 5. 要么 $B^+_r ∩Hd^−_{r'} = ∅$ 要么 $Hd^+_r ∩Hd^+_{r'} = ∅$ 若 $r$ 和 $r'$ 是基本规则，则 $r ≡_s r'$ 当且仅当满足以下条件： 1. $B^−_r = B^−_{r'}$ 2. $Hd^+_r = Hd^+_{r'}$ 3. $Hd^−_r ∪B^+_r = Hd^−_{r'} ∪B^+_{r'}$ 4. 若 $Hd^+_r = Hd^+_{r'} ≠ ∅$，则 $B^+_r = B^+_{r'}$ 且 $Hd^−_r = Hd^−_{r'}$ 基本规则可分为两类：若其正头部非空（$Hd^+_r ≠ ∅$），则不存在其他等价的基本规则；若 $Hd^+_r = ∅$，则 $r$ 可称为约束，它与 $B^+_r ∧Hd^−_r ∧¬B^−_r →⊥$ 强等价，也与通过从约束的正体 $B^+_r ∪Hd^−_r$ 中移除原子并将其否定添加到头部得到的任何规则等价，这被称为移位操作。例如： $p ∧q ∧¬r →⊥≡_s q ∧¬r →¬p ≡_s p ∧¬r →¬q ≡_s ¬r →¬p ∨¬q$ #### 三、通用表格法在答案集编程中的应用 答案集编程（ASP）已成为声明式问题求解的有吸引力的工具，但缺乏描述 ASP 求解器推理的正式框架。我们通过引入通用表格框架来解决这个问题，该框架旨在轻松纳入新的语言构造。 ##### 1. 背景知识 我们采用 Paolo Ferraris 的方法来定义命题理论的答案集语义。命题理论 $\Phi$ 是由字母表 $P$ 中的原子和连接词 $\perp$、$∧$、$∨$、$→$ 构成的有限命题公式集。解释 $X$ 是命题理论 $\Phi$ 的模型，当且仅当 $X |= φ$ 对于所有 $φ ∈\Phi$ 成立。$\Phi$ 相对于 $X$ 的约简 $\Phi^X$ 递归定义如下： $\Phi^X = \{φ^X | φ ∈\Phi\}$ $φ^X = \begin{cases} \perp, & \text{if } X \not|= φ \\ φ, & \text{if } φ ∈X \\ φ^X_1 ◦φ^X_2, & \text{if } X |= φ \text{ and } φ