Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2603.01366 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911478288744448 |
|---|---|
| author | Chen, Peng |
| author_facet | Chen, Peng |
| contents | 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). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_01366 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | NM-DEKL$^3_\infty$: A Three-Layer Non-Monotone Evolving Dependent Type Logic Chen, Peng Logic in Computer Science Computation and Language 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). |
| title | NM-DEKL$^3_\infty$: A Three-Layer Non-Monotone Evolving Dependent Type Logic |
| topic | Logic in Computer Science Computation and Language |
| url | https://arxiv.org/abs/2603.01366 |