一句话：提出直觉主义时态逻辑 ITL^c，证明其可判定，并表明它能表达极小性与庞加莱回归。
Kremer 曾指出，命题线性时态逻辑的语言可在动力系统类上解释，从而得到一种自然的直觉主义时态逻辑。本文引入该逻辑的一个变体 ITL^c，研究其表达力与判定问题。作者证明 ITL^c 是可判定的，并进一步证明动力系统中的极小性（minimality）与庞加莱回归（Poincaré recurrence）都可在 ITL^c 中表达。因此，该逻辑既能刻画非平凡的渐近行为，又保持可判定性，为动力系统提供了一种有表达力的逻辑推理工具。
A dynamical system is a pair $(X,f)$, where $X$ is a topological space and $f\colon X\to X$ is continuous. Kremer observed that the language of propositional linear temporal logic can be interpreted over the class of dynamical systems, giving rise to a natural intuitionistic temporal logic. We introduce a variant of Kremer's logic, which we denote ${\sf ITL^c}$, and show that it is decidable. We also show that minimality and Poincar\'e recurrence are both expressible in the language of ${\sf ITL^c}$, thus providing a decidable logic expressive enough to reason about non-trivial asymptotic behavior in dynamical systems.