NM-DEKL$^3_\infty$: A Three-Layer Non-Monotone Evolving Dependent Type Logic
Logic in Computer Science
2026-03-03 v1 Computation and Language
Abstract
We present a new dependent type system, NM-DEKL (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).
Cite
@article{arxiv.2603.01366,
title = {NM-DEKL$^3_\infty$: A Three-Layer Non-Monotone Evolving Dependent Type Logic},
author = {Peng Chen},
journal= {arXiv preprint arXiv:2603.01366},
year = {2026}
}