关于一阶进展的规模复杂性和可判定性

# 一阶进展的规模复杂性与可判定性¹
¹本文为IJCAI 2026同名论文的扩展版。
来源：https://arxiv.org/html/2605.12691
Daxin Liu² ¹ ² ¹Department of People and Technology, Roskilde University, Denmark ²State Key Laboratory for Novel Software Technology, Nanjing University, China classen@ruc\.dk, daxin\.liu@nju\.edu\.cn

###### 摘要

进展（Progression）是更新知识库以反映动作效果的任务，通常需要二阶逻辑。通过限制知识库或动作效果来识别一阶特殊情况，长期以来一直是动作推理中的核心课题。已知局部效应动作、正常动作和无环动作这三类表达能力递增的动作类均允许一阶进展。然而，对于这些进展的规模（这对实际应用至关重要）缺乏系统分析。本文在情境演算框架下证明，在合理假设下，这些动作类的一阶进展仅以多项式规模增长。此外，我们表明，当知识库属于可判定片段（如二变量一阶逻辑或带常数的全称理论）时，进展仍保持在同一片段内，从而确保了可判定性和实际适用性。

## 1 引言

我们的动机源于使智能体能够在真实场景中行动的目标，这些场景通常具有关于世界状态的不完整信息和无限的对象域。为此，我们使用情境演算（McCarthy and Hayes (1969 (https://arxiv.org/html/2605.12691#bib.bib24)); Reiter (2001 (https://arxiv.org/html/2605.12691#bib.bib23))）这一被广泛研究的一阶形式化框架，用于动作与变化推理。规划、验证和综合等多项推理任务的核心问题是**投影**，即给定一个由描述当前事态的知识库（KB）和编码动作效果的公理组成的理论\(\mathcal{D}\)，确定在执行动作\(\alpha\)后查询公式\(\phi\)是否成立。两种最常见的做法是：通过\(\alpha\)**回归**\(\phi\)，然后检验结果与原知识库的关系；或者通过\(\alpha\)**进展**知识库，然后检验原\(\phi\)与更新后知识库的关系。可以说，回归不太适合实际应用，因为它需要为每个查询公式重新执行，而进展只需为每个动作确定一次即可。

因此，本文重点关注进展。不幸的是，Lin 和 Reiter (1997 (https://arxiv.org/html/2605.12691#bib.bib19)) 给出了一个强烈的负面结果，即表示一阶理论的进展通常需要二阶逻辑。因此，通过限制知识库或动作效果来识别一阶特殊情况，长期以来一直是动作与变化推理中的核心议题。三类表达能力递增²的三个这样的类是：局部效应动作、正常动作（Liu and Lakemeyer (2009 (https://arxiv.org/html/2605.12691#bib.bib2))）和无环动作（Liu and Claßen (2024 (https://arxiv.org/html/2605.12691#bib.bib6))），它们都被证明是可有效一阶进展的。

然而，对于实际可行性，至少有两个额外的方面至关重要，我们将在本文中加以解决。首先，缺乏对这些进展规模复杂性的正式分析。在第2节的形式化预备知识之后，我们在第3节中证明，在特定假设下，前述类别的 FO 进展仅以多项式甚至线性规模增长。此外，我们希望确保查询能够针对进展结果进行有效评估，例如借助一阶逻辑的可判定片段，如二变量片段 \(\text{FO}^2\)（Grädel et al. (1997 (https://arxiv.org/html/2605.12691#bib.bib20))）或带常数的全称理论 \(\text{UTC}\)（Arenas et al. (2018 (https://arxiv.org/html/2605.12691#bib.bib5))）。因此，我们在第4节（\(\text{FO}^2\)）和第5节（\(\text{UTC}\)）中证明这些片段在进展下是封闭的。第6节讨论相关工作并总结。

## 2 预备知识

我们假定熟悉包含等词的一阶逻辑，这里记作 \(\mathcal{L}\)。我们将使用“点”表示法来表示量词后的点具有最大作用范围，例如 \(\forall x.\phi(x)\supset\psi(x)\) 表示 \(\forall x(\phi(x)\supset\psi(x))\)。我们省略开头的全称量词，并假定自由变量是隐式 \(\forall\) 量化的，例如我们将 \(\phi(x)\) 视为 \(\forall x.\phi(x)\)。我们用 \(\phi\Leftrightarrow\psi\) 表示 \(\phi\) 和 \(\psi\) 逻辑等价。我们用 \(\phi(\mu/\mu')\) 表示同时将 \(\phi\) 中表达式（项或公式）\(\mu\) 的每一次出现替换为 \(\mu'\)。设 \(\mathcal{L}^2\) 表示 \(\mathcal{L}\) 的二阶扩展。

### 2.1 情境演算

情境演算（Reiter (2001 (https://arxiv.org/html/2605.12691#bib.bib23))）\(\mathcal{L}_{sc}\) 是一种三域语言，具有一些适合描述动态世界的二阶特性。这些域用于区分**动作**、**情境**和**对象**。\(\mathcal{L}_{sc}\) 使用特定常量 \(S_0\) 表示初始情境；二元函数 \(\mathit{do}(a,s)\) 用于从情境 \(s\) 执行动作 \(a\) 生成后继情境；二元关系 \(\mathit{Poss}(a,s)\) 用于表示动作 \(a\) 在情境 \(s\) 中是可执行的。我们使用 \(a\) 和 \(s\) 作为动作域和情境域的变量。给定一个基动作 \(\alpha\)，我们用 \(S_\alpha\) 表示情境 \(do(\alpha,S_0)\)。**流**是最后一个参数为情境项的谓词；为简化起见，我们省略函数流。一个（可能二价的）公式 \(\phi\) 在情境项 \(s\) 中是**一致的**，如果 \(\phi\) 不提及除 \(s\) 外的任何情境项，不量化任何情境变量，且不提及 \(\mathit{Poss}\)。

###### 定义 1（基本动作理论）.

\(\mathcal{L}_{sc}\) 中的**基本动作理论**（BAT）是一组公理

\[\mathcal{D}= \Sigma_{ind} \cup \mathcal{D}_{ap} \cup \mathcal{D}_{ss} \cup \mathcal{D}_{una} \cup \mathcal{D}_{S_0}, \text{ 其中} \]
1.  \(\Sigma_{ind}\) 是领域无关的公理集（Levesque et al. (1998 (https://arxiv.org/html/2605.12691#bib.bib27))），确保情境结构良好；
2.  \(\mathcal{D}_{ap}\) 是一组动作前提公理；
3.  \(\mathcal{D}_{ss}\) 是一组后继状态公理（SSA），对每个流谓词 \(F\) 形式如下：
    \[F(\vec{x},\mathit{do}(a,s)) \equiv \gamma_F^+(\vec{x},a,s) \lor \neg\gamma_F^-(\vec{x},a,s) \land F(\vec{x},s),\]
    其中 \(\gamma_F^+\) 和 \(\gamma_F^-\) 是使动作 \(a\) 分别导致 \(F\) 为真和为假的条件，这些条件必须在 \(s\) 中一致且满足 \(\mathcal{D}\models \neg(\gamma_F^+ \land \gamma_F^-)\)；
4.  \(\mathcal{D}_{una}\) 是动作的唯一名称公理集：\(A(\vec{x}) \neq A'(\vec{y})\)，以及 \(A(\vec{x})=A(\vec{y})\supset \vec{x}=\vec{y}\)，其中 \(A,A'\) 是不同的动作符号；
5.  \(\mathcal{D}_{S_0}\)，即初始数据库（或初始知识库），是有限个在 \(S_0\) 中一致的句子。

### 2.2 进展

进展应保留所有恰当的信息，即关于初始知识库未来的逻辑蕴含。Lin 和 Reiter (1997 (https://arxiv.org/html/2605.12691#bib.bib19)) 给出了进展的模型论定义，并证明进展是可二阶定义的。Vassos 和 Levesque (2013 (https://arxiv.org/html/2605.12691#bib.bib18)) 证明任何正确的进展都等价于 Lin 和 Reiter (1997 (https://arxiv.org/html/2605.12691#bib.bib19)) 的二阶表示。这里我们采用 Vassos 和 Levesque (2013 (https://arxiv.org/html/2605.12691#bib.bib18)) 的定义。

设 \(\mathcal{D}_{ss}[\alpha,S_0]\) 是 \(\mathcal{D}_{ss}\) 关于 \(\alpha\) 和 \(S_0\) 的实例化，即
\[\mathcal{D}_{ss}[\alpha,S_0] \Leftrightarrow \bigwedge_{F} \forall \vec{x}.\, F(\vec{x},\mathit{do}(\alpha,S_0)) \equiv \Phi_F(\vec{x},\alpha,S_0),\]
其中 \(\Phi_F\) 表示流 \(F\) 的 SSA 的右端。设 \(F_1,\ldots,F_n\) 是所有流的集合。对每个流 \(F_i\)，我们引入一个新的谓词符号 \(P_i\)。设 \(\phi \uparrow S_0\) 是将 \(\phi\) 中的每个 \(F_i(\vec{t},S_0)\) 替换为 \(P_i(\vec{t})\) 的结果，并称 \(P_i\) 为 \(F_i\) 的**提升谓词**。对于有限公式集 \(\Sigma\)，我们也用 \(\Sigma\) 表示其元素的合取。

###### 定义 2.

设 \(\mathcal{D}\) 是一个基本动作理论，\(\alpha\) 是在 \(\mathcal{D}_{ap}\) 下可执行的基动作，\(\mathcal{D}_{S_\alpha}\) 是 \(S_\alpha\) 中的一组一致的（一阶或二阶）句子。我们说 \(\mathcal{D}_{S_\alpha}\) 是 \(\mathcal{D}_{S_0}\) 相对于 \(\alpha,\mathcal{D}\) 的**进展**，当且仅当

\[\mathcal{D}_{una} \cup \mathcal{D}_{S_\alpha} \Leftrightarrow \mathcal{D}_{una} \land
\exists \vec{R}.\{ (\mathcal{D}_{S_0} \cup \mathcal{D}_{ss}[\alpha,S_0]) \uparrow S_0 \}(\vec{P}/\vec{R})  \tag{1}\]
其中 \(\vec{R}=\{R_1,\ldots,R_n\}\) 是二阶谓词变量。

定义2是正确的，因为对于任何在 \(S_\alpha\) 中一致的 \(\phi\)，如果 \(\mathcal{D}_{S_\alpha}\) 是 \(\mathcal{D}_{S_0}\) 相对于 \(\alpha,\mathcal{D}\) 的进展，则
\(\mathcal{D} \models \phi\) 当且仅当 \((\mathcal{D}-\mathcal{D}_{S_0}) \cup \mathcal{D}_{S_\alpha} \models \phi\)（Vassos and Levesque, 2013 (https://arxiv.org/html/2605.12691#bib.bib18)，定理1）。

### 2.3 遗忘

识别情境演算中进展可一阶定义的片段有两种方法：一种限制初始理论的结构，另一种限制动作效果。本文关注后者，特别是**局部效应动作理论**（BAT-LE）、**正常动作理论**（BAT-NR）和**无环动作理论**（BAT-AC）。后续几节给出这些类别的定义，介绍相关的进展方法，并提供规模复杂性结果作为新贡献。

一个理论通过一个动作的进展可以解释为**遗忘**关于原始世界状态的所有信息，只保留与新状态相关的信息。直观上，遗忘理论中的一个基原子（或谓词）会导致一个更弱的理论，该理论蕴含同一组与原子（或谓词）“无关”的句子。对于句子 \(\phi\) 和基原子 \(P(\vec{t})\)，设 \(\phi[P(\vec{t})]\) 是通过将 \(\phi\) 中每个形如 \(P(\vec{t}')\) 的出现替换为 \([\vec{t}=\vec{t}' \land P(\vec{t})] \lor [\vec{t}\neq\vec{t}' \land P(\vec{t}')]\) 得到的公式。显然，\(\phi \Leftrightarrow \phi[P(\vec{t})]\)。设 \(\phi_+^{P(\vec{t})}\) 和 \(\phi_-^{P(\vec{t})}\) 是通过分别将 \(\phi[P(\vec{t})]\) 中的 \(P(\vec{t})\) 替换为 \(true\) 和 \(false\) 得到的公式。

###### 定理 3（Lin and Reiter (1994 (https://arxiv.org/html/2605.12691#bib.bib7))）.

设 \(P(\vec{t})\) 是基原子，\(P\) 是谓词符号，\(\phi\) 是句子。那么

- \(\mathit{forget}(\phi,P(\vec{t})) \Leftrightarrow \phi_+^{P(\vec{t})} \lor \phi_-^{P(\vec{t})}\);
- \(\mathit{forget}(\phi,P) \Leftrightarrow \exists R.\, \phi(P/R)\)，其中 \(R\) 是二阶变量。

因此，式 (1) 中的进展等价于添加动作效果 (\(\mathcal{D}_{ss}[\alpha,S_0]\)) 并遗忘流在情境 \(S_0\) 下的真值（由外部的 \(\exists\) 量化）。因此，在式 (1) 中的二阶量词可消除的情况下，进展可一阶定义。

不失一般性，我们假设 SSA 中的 \(\gamma_F^\pm(\vec{x},a,s)\) 是形如（对每个动作符号 \(A\) 有一个合取项）的析取式：

\[\exists \vec{z}. \bigl( a = A(\vec{v}) \land \phi_A^\pm(\vec{x},\vec{z},s) \bigr)\]
其中 \(A(\vec{v})\) 是动作项，\(\vec{v}\) 可能包含 \(\vec{x}\) 中的某些变量，其余变量为 \(\vec{z}\)；\(\phi_A^\pm(\vec{x},\vec{z},s)\) 是在 \(s\) 中一致且不含动作项的公式，所有自由变量符号在 \(\vec{x},\vec{z},s\) 中。在此假设和 \(\mathcal{D}_{una}\) 下，对每个基动作 \(\alpha = A(\vec{t})\)，

\[\gamma_F^\pm(\vec{x},\alpha,S_0) \Leftrightarrow \exists \vec{z}. \bigl( \vec{t}=\vec{v} \land \phi_A^\pm(\vec{x},\vec{z},S_0) \bigr). \tag{2}\]
此后，每当引用 \(\gamma_F^\pm(\vec{x},\alpha,S_0)\)，我们都指式 (2) 的右端，这对 \(\mathcal{D}_{ss}[\alpha,S_0]\) 同样适用。

## 3 进展的规模复杂性

先前关于无环动作理论 FO 进展的工作（Liu and Claßen (2024 (https://arxiv.org/html/2605.12691#bib.bib6))）在计算时间方面确定了一些复杂性结果。然而，结果理论的规模同样关键，因为它直接影响针对该理论进行查询检验的计算成本。这里，我们确定 BAT-LE、BAT-NR 和 BAT-AC 理论 FO 进展规模的上界。

形式上，公式 \(\phi\) 的规模 \(\|\phi\|\) 是它所包含的原子（包括等式）、布尔连接词（来自 \(\{\land,\lor,\lnot\}\)）和量词（来自 \(\{\exists,\forall\}\)）的数量。如前所述，带自由变量的公式视为其全称闭包。在可能的情况下，开头的全称量词被省略，不计入规模。而且，通常我们将有限理论视为其中所含公式的合取。为避免混淆，当我们谈论这种有限理论的规模时，总是指它所呈现的公式的规模，**而不是**集合中公式的数量。

Th