2026-10-10T21:17:37Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27700 2026-10-10T19:48:19Z ddc:004 open_access

Discrete Linear Ensemble Logic: Decidability, Expressiveness, and Axiomatization Droste, Manfred Zhang, Guo-Qiang Temporal logic monadic Presburger arithmetic descriptive complexity electronic health records We study the discrete point-based fragment of Ensemble Logic EL(ℕ) over the natural numbers, a logic combining displacement φ_u, term-dependent metric modalities ☐_t and ♢_t with respect to an additive term t, Boolean connectives, and first-order quantification over ℕ. Motivated by the need for a unified symbolic representation of biomedical knowledge with temporal, spatial, and multimodal metric content, we develop the foundational discrete theory of the formalism. We give syntax and semantics, and prove a forward embedding of EL(ℕ) (over a finite proposition set 𝒫) into first-order monadic Presburger arithmetic FO(ℕ,<,+;𝒫). This embedding yields the analytical upper bounds, while a reduction from nondeterministic two-counter Turing machines with recurring control states proves that satisfiability is Σ¹₁-complete and validity is dually Π¹₁-complete. Expressively, EL(ℕ) strictly extends the star-free ω-languages and is incomparable with the ω-regular languages: it defines the non-ω-regular counting language {a^m b^m c^m d^m∣ m ≥ 1}⋅Σ^ω, whereas a delimited parity language remains outside the logic by a quantifier-bounding argument combined with classical circuit lower bounds for parity. On the proof-theoretic side, we present a sound Hilbert system ℋ_EL and establish completeness relative to monadic Presburger validity as oracle, noting that completeness relative to plain Presburger arithmetic is impossible. We also prove that the existential fragment ∃EL(ℕ) has NP-complete satisfiability and coNP-complete unsatisfiability. Finally, we show that finite active-domain model-checking has PTIME data complexity and PSPACE-complete combined complexity. Together, these results give a precise decidability, expressiveness, proof-theoretic, and model-checking baseline for subsequent algorithmic applications of Ensemble Logic in biomedicine. This work is a part of the Symbolic Biomedicine program championed by the corresponding author. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Manfred Droste and Guo-Qiang Zhang 2026 Is Part Of OASIcs, Volume 146, 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.TIME.2026.4 urn:nbn:de:0030-drops-277009 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.4 eng https://creativecommons.org/licenses/by/4.0/legalcode