知识与行为更新语言：KABUL语义解析

# 知识与行为更新语言：KABUL语义解析 ## 1. 基础概念 ### 1.1 关键定义 - **once_retract_event (R)**：与 retract_event (R) 相同，并且，如果条件 Cond 在当前状态不成立，语句 ^ 将被添加到后继状态的自我更新中，除非同时执行了 [always_ | once_] retract (\l>) 形式的命令。 - **更新程序**：KABUL 中的更新程序是一组语句。 - **查询**：对知识库的查询是一种命题表达式，形式为 holds(Li, ..., Lk, in(Ri), ..., in(Rm), out(Rm + 1), ..., out(Rn)) at q ? ，其中 Li 是文字，Ri 是规则，q 是一个状态且 q < s（s 是当前状态），若 q = s，查询中常省略 “at q”。 ### 1.2 确定后继知识库状态的步骤 确定后继知识库状态 (Ps + 1, SUs + 1) 需要分三步进行： 1. 相对于外部观察集和当前对象级知识库，部分评估 SUS 和 EUs + 1 中的语句，以确定两个更新程序约简。 2. 根据先前获得的约简，确定一组要执行的命令。 3. 确定下一个状态的知识库。 ### 1.3 过渡框架 过渡框架是一个元组 (Ps, |=, SUs, EUs + 1, EOs + 1, <, Sel(.))，其中 Ps、SUs、EUs + 1 和 EOs + 1 如前文定义，|= 是对应于对象知识库 “Ps” 语义的后果运算符，Sel(.) 是一个选择函数，用于从可能的命令集中返回一个集合。 ### 1.4 更新程序拆分 每个更新程序（SUS 和 EUs + 1）根据语句的头部拆分为两个集合： - **正更新 U +**：U + = {C0(p) <= Cond e U} - **抑制更新 U -**：U - = {notCo(p) <= Cond e U} 例如，对于包含特定语句的更新程序 U，其 U + 和 U - 分别包含不同的语句，具体如下： ```plaintext U 包含语句： always_assert (always_assert_event (b <— d) <= E : in(obs (d))) <= E : in(obs (b)) always_assert (R) <= R : out(R),E : in(rule(R)) always_assert_event (b <— d) <= not assert (a), a, not b not assert (c <— d) <= not b, E : in(obs (b)) assert_event (a <— h) <= not assert (a), not a, b U + 包含语句： always_assert (always_assert_event (b <— d) <= E : in(obs (d))) <= E : in(obs (b)) always_assert (R) <= R : out(R), E : in(rule(R)) always_assert_event (b <— d) <= not assert (a), a, not b assert_event (a <— h) <= not assert (a), not a, b U - 包含语句： not assert (c <— d) <= not b, E : in(obs (b)) ``` ## 2. 更新程序约简 ### 2.1 评估方法 部分评估 SUS 和 EUs + 1 中的语句时，有三种可能的评估方法： - **怀疑方法**：使用所有稳定模型的交集来确定每个语句的可执行性。例如，对于一个具有特定规则的动态逻辑程序和包含三个语句的更新，初始逻辑程序有两个稳定模型 M1 = {a, c} 和 M2 = {b, c}，使用怀疑方法时，仅使用交集 {c} 评估条件，只有 assert (f) <= c 的条件会被积极评估，f 将被断言到知识库中。 - **轻信方法**：使用所有稳定模型的并集来确定每个语句的可执行性。在上述例子中，使用 {a, b, c} 评估条件，所有三个语句的条件都会被积极评估，d、e 和 f 都会被断言到知识库中，但这种方法可能导致矛盾，不适合此类更新。 - **个案方法**：分别考虑每个稳定模型，每个模型可能产生不同的要执行的命令集。在上述例子中，考虑稳定模型 {a, c} 时断言 d 和 f，考虑稳定模型 {b, c} 时断言 e 和 f。 ### 2.2 选择怀疑方法的原因 - 避免知识库数量指数级增长：使用个案方法会使要考虑的知识库数量呈指数级增长，而我们的目标是在每次状态转换后定义一个单一的知识库。 - 语义定义可扩展性：怀疑方法的语义定义可以轻松扩展到处理多个模型和多组可执行命令的情况。 - 历史原因：最初 LUPS 的作者选择了怀疑方法。 ### 2.3 部分评估的语义 - **文字**：文字的评估与之前相同，即文字的合取 L (S) = Li, ..., Lk 评估为真，当且仅当 ⊗Ps |=sm Li, ..., Lk。 - **规则**：通过评估对象知识库中相应的辅助谓词 AT(_) 来评估语句 S 中规则在对象知识库中的记忆存在或不存在的条件。例如，in(R) 评估为真，如果规则 R 被惯性断言到知识库中且自最近一次断言后未被撤销，或者在先前的状态转换期间被非惯性断言。 - **观察**：通过简单检查它们在集合 EOs + 1 中的存在或不存在来评估语句 S 的外部观察条件 E (S)。 ### 2.4 更新程序约简定义 更新程序 U 相对于外部观察集 EO 和状态 s 处的动态逻辑程序 Ps 的约简 Ur 定义为： Ur = {H (S) <= C (S) : (H (S) <= C (S), L (S), R : R (S), E : E (S)) e U, ⊗Ps |=sm L (S) ∧ ⊗Ps |=rule R (S) ∧ EO |=obs E (S)} 例如，给定特定的 Ps、EOs + 1 和 U，可计算出 U 的约简 Ur 及其正约简 Ur + 和抑制约简 Ur - ： ```plaintext Ps 的唯一稳定模型： Ms = {a, not b, c, N(b <— a), not N(not b <— a), not N(a <— ), ...} EOs + 1： EOs + 1 = {obs (d), obs (b), rule(not b <— a), rule(b <— a)} U 包含语句： always_assert (always_assert_event (b <— d) <= E : in(obs (d))) <= E : in(obs (b)) always_assert (R) <= R : out(R),E : in(rule(R)) always_assert_event (b <— d) <= not assert (a), a, not b not assert (c <— d) <= not b, E : in(obs (b)) assert_event (a <— h) <= not assert (a), not a, b Ur 包含语句： always_assert (always_assert_event (b <— d) <= E : in(obs (d))) <= always_assert (not b <— a) <= always_assert_event (b <— d) <= not assert (a) not assert (c <— d) <= Ur + 包含语句： always_assert (always_assert_event (b <— d) <= E : in(obs (d))) <= always_assert (not b <— a) <= always_assert_event (b <— d) <= not assert (a) Ur - 包含语句： not assert (c <— d) <= ``` ## 3. 可执行命令 ### 3.1 相关定义 - **规则参数**：ArgsR (Ur) 是 Ur 中命令（和抑制命令）中作为参数出现的所有规则的集合。 - **语句参数**：Argss (Ur) 是 Ur 中命令（和抑制命令）中作为参数出现的所有语句的集合。 - **基本规则命令**：BasicCommR(Ur) 是包含 as