Document Open Access Logo

Discrete Linear Ensemble Logic: Decidability, Expressiveness, and Axiomatization

Authors Manfred Droste , Guo-Qiang Zhang

PDF

File

Thumbnail PDF
PDF
OASIcs.TIME.2026.4.pdf
  • Filesize: 0.93 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Logic and verification
  • Theory of computation → Algebraic language theory
  • Applied computing → Health informatics
Keywords
  • Temporal logic
  • monadic Presburger arithmetic
  • descriptive complexity
  • electronic health records

Metrics

Abstract

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.

Cite As Get BibTex

Manfred Droste and Guo-Qiang Zhang. Discrete Linear Ensemble Logic: Decidability, Expressiveness, and Axiomatization. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/OASIcs.TIME.2026.4

Author Details

Manfred Droste
  • Institute of Computer Science, Leipzig University, Germany
Guo-Qiang Zhang
  • The University of Texas Health Science Center at Houston, TX, USA

Funding

  • Zhang, Guo-Qiang: This work has been supported in part by the U.S. National Science Foundation Award IIS2500624 and the National Institutes of Health grants R01AG084236 and U24AG098157. The views of the paper are those of the authors and do not reflect those of the funding agencies.

Acknowledgements

Part of this research was done during a research stay of MD in April 2026 at the University of Texas Health Science Center at Houston. He would like to thank his colleagues for a fruitful and most enjoyable time.

References

  1. Miklós Ajtai. Σ¹₁-formulae on finite structures. Annals of Pure and Applied Logic, 24(1):1-48, 1983. URL: https://doi.org/10.1016/0168-0072(83)90038-6.
  2. James F. Allen. Maintaining knowledge about temporal intervals. Communications of the ACM, 26(11):832-843, 1983. URL: https://doi.org/10.1145/182.358434.
  3. Rajeev Alur and Thomas A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181-204, 1994. URL: https://doi.org/10.1145/174644.174651.
  4. Olivier Bodenreider. The Unified Medical Language System (UMLS): integrating biomedical terminology. Nucleic Acids Research, 32(Database issue):D267-D270, 2004. URL: https://doi.org/10.1093/nar/gkh061.
  5. Davide Bresolin, Angelo Montanari, Pietro Sala, and Guido Sciavicco. What’s decidable about Halpern and Shoham’s interval logic? The maximal fragment ABBL. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS 2011), pages 387-396. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/LICS.2011.35.
  6. D. C. Cooper. Theorem proving in arithmetic without multiplication. In Bernard Meltzer and Donald Michie, editors, Machine Intelligence, volume 7, pages 91-99. Edinburgh University Press, Edinburgh, 1972. Google Scholar
  7. S. Shelah D. Gabbay, A. Pnueli and J. Stavi. On the temporal analysis of fairness. In Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages (POPL), 1980, pages 163-173. ACM Press, 1980. URL: https://doi.org/10.1145/567446.567462.
  8. Emek Demir et al. The BioPAX community standard for pathway data sharing. Nature Biotechnology, 28(9):935-942, 2010. URL: https://doi.org/10.1038/nbt.1666.
  9. J. Fan, Xiaojin Li, Yan Huang, X. Hao, Licong Cui, and Guo-Qiang Zhang. Ensemble logic for symbolic representation of sleep medicine guidelines. In Proceedings of the AMIA 2026 Annual Symposium, 2026. In press, 10 pages. URL: https://doi.org/10.48550/arXiv.2607.21331.
  10. Merrick L. Furst, James B. Saxe, and Michael Sipser. Parity, circuits, and the polynomial-time hierarchy. Mathematical Systems Theory, 17(1):13-27, 1984. URL: https://doi.org/10.1007/BF01744431.
  11. Joseph Y. Halpern. Presburger arithmetic with unary predicates is Π¹₁ complete. Journal of Symbolic Logic, 56(2):637-642, 1991. URL: https://doi.org/10.2307/2274706.
  12. Joseph Y. Halpern and Yoav Shoham. A propositional modal logic of time intervals. Journal of the ACM, 38(4):935-962, 1991. URL: https://doi.org/10.1145/115234.115351.
  13. David Harel, Amir Pnueli, and Jonathan Stavi. Propositional dynamic logic of nonregular programs. Journal of Computer and System Sciences, 26(2):222-243, 1983. URL: https://doi.org/10.1016/0022-0000(83)90014-4.
  14. Johan Håstad. Almost optimal lower bounds for small depth circuits. In Proceedings of the 18th Annual ACM Symposium on Theory of Computing (STOC 1986), pages 6-20. ACM, 1986. URL: https://doi.org/10.1145/12130.12132.
  15. Yan Huang, Xiaojin Li, Licong Cui, and Guo-Qiang Zhang. A logic-based temporal cohort discovery engine: algorithms, indices, and experimental results on the National Sleep Research Resource. Journal of Biomedical Informatics, 2026. Under review. URL: https://doi.org/10.48550/arXiv.2607.21377.
  16. Yan Huang, Xiaojin Li, X. Hao, Rashmie Abeysinghe, Licong Cui, and Guo-Qiang Zhang. Scaling up formal representation of clinical trial protocols in ensemble logic using LLMs: a preliminary study. In Proceedings of the AMIA 2026 Annual Symposium, 2026. In press, 10 pages. URL: https://doi.org/10.48550/arXiv.2607.21307.
  17. Michael Hucka et al. The Systems Biology Markup Language (SBML): a medium for representation and exchange of biochemical network models. Bioinformatics, 19(4):524-531, 2003. URL: https://doi.org/10.1093/bioinformatics/btg015.
  18. Hans Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, Los Angeles, 1968. URL: https://philpapers.org/rec/KAMTLA-2.
  19. Ron Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255-299, 1990. URL: https://doi.org/10.1007/BF01995674.
  20. Xiaojin Li, Yan Huang, Rashmie Abeysinghe, Zenan Sun, Hongyu Chen, Pengze Li, Xing He, Shiqiang Tao, Cui Tao, Jiang Bian, Licong Cui, and Guo-Qiang Zhang. Temporal Ensemble Logic for Integrative Representation of the Entirety of Clinical Trials. In Thierry Vidal and Przemysław Andrzej Wałęga, editors, 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025), volume 355 of Leibniz International Proceedings in Informatics (LIPIcs), pages 13:1-13:16, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TIME.2025.13.
  21. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs, NJ, 1967. Google Scholar
  22. Joël Ouaknine and James Worrell. On the decidability of metric temporal logic. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005), pages 188-197. IEEE Computer Society, 2005. URL: https://doi.org/10.1109/LICS.2005.33.
  23. Christos H. Papadimitriou. On the complexity of integer programming. Journal of the ACM, 28(4):765-768, 1981. URL: https://doi.org/10.1145/322276.322287.
  24. Amir Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS 1977), pages 46-57, Providence, RI, 1977. IEEE. URL: https://doi.org/10.1109/SFCS.1977.32.
  25. Mojżesz Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Comptes Rendus du I Congrès des Mathématiciens des Pays Slaves, pages 92-101, Warsaw, 1929. URL: https://eudml.org/doc/212367.
  26. Jean Serra and Pierre Soille, editors. Mathematical Morphology and Its Applications to Image Processing, volume 2 of Computational Imaging and Vision. Kluwer Academic Publishers, Dordrecht, 1994. URL: https://doi.org/10.1007/978-94-011-1040-2.
  27. U.S. National Library of Medicine. Effect of Different Doses of SAR110894 on Cognition in Patients with Mild to Moderate Alzheimer’s Disease on Donepezil. ClinicalTrials.gov, 2011. ClinicalTrials.gov Identifier: NCT01266525. URL: https://clinicaltrials.gov/study/NCT01266525.
  28. Guo-Qiang Zhang. Temporal Ensemble Logic. CoRR, abs/2408.14443, 2024. URL: https://doi.org/10.48550/arXiv.2408.14443.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact