NM-DEKL$^3_\infty$：一种三层非单调依赖类型逻辑
NM-DEKL$^3_\infty$: A Three-Layer Non-Monotone Evolving Dependent Type Logic
AI总结：
NM-DEKL$^3_\infty$是一种用于形式化动态环境中演化知识的三层非单调依赖类型系统，具备正确性、等价完备性及对μ-演算的嵌入能力。
摘要：
我们提出了一种新的依赖类型系统NM-DEKL$^3_\infty$（非单调依赖知识增强逻辑），用于在动态环境中形式化演化的知识。该系统采用三层架构，分别分离了计算层、构造性知识层和命题知识层。我们定义了其语法和语义，并建立了正确性和等价完备性；我们构建了一个语法模型，并证明其在模型类别中是初始的，从而得出等价完备性。我们还给出了嵌入到μ-演算中的方法，并给出了严格的表达性包含（包括非双射不变属性的表达能力）。
英文摘要：
We present a new dependent type system, NM-DEKL$^3_\infty$ (Non-Monotone Dependent Knowledge-Enhanced Logic), for formalising evolving knowledge in dynamic environments. The system uses a three-layer architecture separating a computational layer, a constructive knowledge layer, and a propositional knowledge layer. We define its syntax and semantics and establish Soundness and Equational Completeness; we construct a syntactic model and prove that it is initial in the category of models, from which equational completeness follows. We also give an embedding into the $μ$-calculus and a strict expressiveness inclusion (including the expressibility of non-bisimulation-invariant properties).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
