# Temporal Ensemble Logic

arXiv: https://arxiv.org/abs/2408.14443 · HTML: https://mlsanity.com/paper/2408.14443/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Placed in Knowledge- and tool-augmented reasoning, one of 17 directions in LLM reasoning.
- Builds on 4 of its 54 references that are in the map.
- First posted on arXiv 26 Aug 2024.

## Placed in

- LLM reasoning / [Knowledge- and tool-augmented reasoning](https://mlsanity.com/lr/knowledge-and-tool-augmented-reasoning/)

## Builds on (most cited first, 4 of 4)

- [Deciding Hyperproperties](https://mlsanity.com/paper/1606.07047/) (2016)
- [One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata](https://mlsanity.com/paper/1805.00748/) (2018)
- [Efficient Genomic Interval Queries Using Augmented Range Trees](https://mlsanity.com/paper/1806.01217/) (2018)
- [Computational Logic for Biomedicine and Neurosciences](https://mlsanity.com/paper/2007.07571/) (2020)

## Built on by (most cited first, 2 of 2)

- [AD-CDO: A Lightweight Ontology for Representing Eligibility Criteria in Alzheimer's Disease Clinical Trials](https://mlsanity.com/paper/2511.21724/) (2025)
- [Scaling Up Formal Representation of Clinical Trial Protocols in Ensemble Logic Using LLMs: A Preliminary Study](https://mlsanity.com/paper/2607.21307/) (2026)

## Abstract (arXiv)

We introduce Temporal Ensemble Logic (TEL), a monadic, first-order modal logic for linear-time temporal reasoning. TEL includes primitive temporal constructs such as ``always up to t time later'' (Boxt), ``sometimes before t time in the future'' (Diamondt), and ``t-time later'' varphit. TEL has been motivated from the requirement for rigor and reproducibility for cohort specification and discovery in clinical and population health research, to fill a gap in formalizing temporal reasoning in biomedicine. Existing logical frameworks such as linear temporal logic are too restrictive to express temporal and sequential properties in biomedicine, or too permissive in semantic constructs, such as in Halpern-Shoham logic, to serve this purpose. In this paper, we first introduce TEL in a general set up, with discrete and dense time as special cases. We then focus on the theoretical development of discrete TEL on the temporal domain of positive integers mathbbN^+, denoted as rm TEL_mathbbN^+. rm TEL_mathbbN^+ is strictly more expressive than the standard monadic second order logic, characterized by B"uchi automata. We present its formal semantics, a proof system, and provide a proof for the undecidability of the satisfiability of rm TEL_mathbbN^+. We also include initial results on expressiveness and decidability fragments for rm TEL_mathbbN^+, followed by application outlook and discussions.