提出三层非单调依赖逻辑，形式化动态环境中的演化知识。
NM-DEKL$^3_\infty$: A Three-Layer Non-Monotone Evolving Dependent Type Logic
- 三层架构分离计算、构造性知识与命题知识
- 证明了系统的可靠性与等式完备性
- 可嵌入μ-演算，能表达非双模不变性质
我们提出一种新的依赖类型系统NM-DEKL$^3_ inity$（非单调依赖知识增强逻辑），用于在动态环境中形式化演化知识。该系统采用三层架构，分别包含计算层、构造性知识层和命题知识层。我们定义了其语法与语义，并建立了可靠性和等式完备性；构造了一个句法模型，并证明其在模型范畴中为初始对象，从而推出等式完备性。此外，我们给出了向μ-演算的嵌入，并证明了严格表达力包含关系（包括非双模不变性质的可表达性）。
原文摘要 · Abstract (English)
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).
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。