DEKL 2.0: Trace-Indexed Knowledge Evolution in Dependent Type Theory

TL;DR

DEKL 2.0 introduces a dependent type-theoretic framework that models trace-indexed knowledge evolution, combining categorical semantics with support for non-monotonic reasoning and fixed points.

Contribution

It provides a novel dependent type-theoretic approach unifying executable traces, typed witnesses, and knowledge revision with categorical semantics.

Findings

Proof calculus remains monotone under structural rules.

Finite and infinite traces are first-class objects.

Semantic interpretation uses free categories from transition systems.

Abstract

DEKL 2.0 is a dependent type-theoretic framework for trace-indexed knowledge evolution. Its central claim is that the proof calculus remains monotone under standard structural rules, while non-monotonic behavior arises semantically from trace extension. Finite and infinite traces are first-class objects in the computational universe; knowledge is interpreted as a presheaf over the finite-trace category; and proposition-level reasoning is handled categorically with fixed-point support. We establish trace--reachability correspondence and completeness, characterize non-monotonicity by non-surjective restriction maps, and present a semantic interpretation based on the free category generated by a transition system. The framework unifies executable traces, typed witnesses, and knowledge revision in one dependent language.