非标准推理扩展与子集空间拓扑性质的模态逻辑研究

### 非标准推理扩展与子集空间拓扑性质的模态逻辑研究 #### 简单描述图到FLE + 概念描述的转换 在描述逻辑中，存在一些描述图没有等价的FLE + 概念描述。不过，我们可以将反向翻译过程限制在简单描述图的类别上。 反向翻译过程不能依赖图标签集中的复杂概念描述，而是要在保留与原始描述图等价性的前提下，重新构建标签集中的复杂概念描述，直到所需的概念描述出现在根标签中。这与FLE + 描述图的生成过程相反，在生成过程中，根顶点的标签会生成整个描述图。 为了形式化重新构建复杂标签的概念，我们定义了一个操作`acc`，它通过改变描述图的标签函数来修改给定的描述图。直观上，`acc`函数会在顶点的标签集中“积累”复杂概念描述。 设$G := (V, E, v_0, ℓ_V, ℓ_E)$为一个描述图，且$|E| := n$。则$acc(G) := (V, E, v_0, ℓ'_V, ℓ_E)$，其中$ℓ'_V$的定义如下：对于每个$v \in V$， \[ ℓ'_V(v) := (ℓ_V(v) \cap N_C ) \cup \bigcup_{r \in N_R \cup N_T^R} \left( \bigcup_{(v \exists r w) \in E} \exists r. \bigcap ℓ_V(w) \cup \bigcup_{(v \forall r w) \in E} \left( \forall r. \bigcap(ℓ_V(w) \setminus \{ \forall r. \top \}) \cap \bigcap_{(w \exists r w') \in E} \exists r. \bigcap ℓ_V(w') \right) \right) \] 定义$conc(G) := \bigcap ℓ_V(v'_0)$，其中$v'_0$表示$acc^n(G)$的根顶点。 对于每个顶点$v$，修改后的标签函数$ℓ'_V$包含与之前相同的原子标签，但额外增加了基于$v$的每个$\exists r$后继标签的存在性限制。对于全称边，处理方式类似，但还会考虑从通过全称边可达的顶点出发的存在性边。 例如，考虑一个简单描述图$G$，它只有一个顶点$v_0$，标签为$ℓ_V(v_0) = \{A\}$，边集为$E := \{(v_0, \exists r, v_0), (v_0 \forall r v_0)\}$。在图$acc(G)$中，根顶点的标签为$\{A, \exists r.A, \forall r.(A \cap \exists r.A)\}$。再次应用$acc$函数，$acc^2(G)$的根标签为$\{A, \exists r.(A \cap \exists r.A \cap \forall r.(A \cap \exists r.A)), \forall r.(A \cap \exists r.A \cap \forall r.(A \cap \exists r.A) \cap \exists r.(A \cap \exists r.A \cap \forall r.(A \cap \exists r.A)))\}$。 可以证明，最多应用$|E|$次$acc$函数会产生一个根标签，使得其中所有概念的合取与原描述图$G$等价。因此，我们得到定理：对于每个简单描述图$G = (V, E, v_0, ℓ_V, ℓ_E)$，有$conc(G) \equiv G$。证明该定理的思路分为三步： 1. 对于每个$G$，单次应用$acc$函数能保持等价性，即$G \equiv acc(G)$，这直接意味着$G \equiv acc^{|E|}(G)$。 2. 根据描述图的语义，容易看出$acc^{|E|}(G)$根标签中的每个概念描述都包含$acc^{|E|}(G)$，即$acc^{|E|}(G) \subseteq conc(G)$。 3. 可以证明$conc(G)$的每个模型也是$acc^{|E|}(G)$的模型。 #### FLE + 中包含关系的刻画 利用前面介绍的描述图，可以刻画FLE + 概念描述的包含关系。定理表明，对于FLE + 概念描述$C$和$D$，$C \subseteq D$当且仅当$G_D \rightrightarrows G_C$。 为了证明“如果”方向，可以使用从$G_C$通过将$E_C$中所有边$