Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

NM-DEKL$^3_\infty$: A Three-Layer Non-Monotone Evolving Dependent Type Logic

Peng Chen

TL;DR

A new dependent type system, NM-DEKL$^3_\infty$ (Non-Monotone Dependent Knowledge-Enhanced Logic), for formalising evolving knowledge in dynamic environments and establishes Soundness and Equational Completeness.

Abstract

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).

NM-DEKL$^3_\infty$: A Three-Layer Non-Monotone Evolving Dependent Type Logic

TL;DR

A new dependent type system, NM-DEKL (Non-Monotone Dependent Knowledge-Enhanced Logic), for formalising evolving knowledge in dynamic environments and establishes Soundness and Equational Completeness.

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).
Paper Structure (199 sections, 43 theorems, 124 equations)

This paper contains 199 sections, 43 theorems, 124 equations.

Table of Contents

  1. Introduction
  2. Relation to Existing Systems
  3. Syntax of NM-DEKL$^3_\infty$
  4. Notational Conventions
  5. Three Universes and Stratification
  6. Computational Layer $\mathsf{Uc}$ and Traces
  7. Basic Types
  8. Finite Traces (Inductive)
  9. Infinite Traces (Coinductive)
  10. Constructive Knowledge Layer $\mathsf{Type}_\ell$ and Non-Monotonicity
  11. Knowledge Families
  12. Trajectory Extension
  13. Non-Monotonic Restriction Rule
  14. Identity Types
  15. Constructive Knowledge and Causal Reasoning
  16. ...and 184 more sections

Key Result

Theorem 2.2

In NM-DEKL$^3_\infty$, the constructive layer can represent not only types but also richer logical reasoning via causal chains and trace structure, including dynamic, causal, and history-dependent reasoning.

Theorems & Definitions (99)

  • Definition 2.1: Causal Reasoning
  • Theorem 2.2: Constructive Knowledge and Logical Reasoning
  • proof : Proof idea
  • Definition 2.3: Definitional equality $\equiv$
  • Definition 2.4: Failure
  • Theorem 2.5: Relation between non-monotonicity and failure
  • proof
  • Lemma 2.6: Substitution Lemma
  • Theorem 3.1: Strong normalisation for $\mathsf{Uc}$
  • proof : Proof idea
  • ...and 89 more