标题： LeanLTL：Lean 中线性时态逻辑的统一框架 显示英文标题

标题： LeanLTL: A unifying framework for linear temporal logics in Lean

摘要： 我们提出LeanLTL，这是一个在Lean 4中的线性时序逻辑的统一框架。 LeanLTL支持对代表无限或有限线性时间的轨迹进行推理。 该库允许传统的LTL语法与任意的Lean表达式结合，使得定义涉及数值或其他类型的属性变得简单。 我们证明了标准的LTL变体可以嵌入到我们的框架中。 该库还提供了以促进使用Lean现有战术的方式对LeanLTL公式进行推理的自动化功能。 最后，我们提供了示例，说明该库在处理来自应用的系统推理中的实用性。 显示英文摘要

摘要： We propose LeanLTL, a unifying framework for linear temporal logics in Lean 4. LeanLTL supports reasoning about traces that represent either infinite or finite linear time. The library allows traditional LTL syntax to be combined with arbitrary Lean expressions, making it straightforward to define properties involving numerical or other types. We prove that standard flavors of LTL can be embedded in our framework. The library also provides automation for reasoning about LeanLTL formulas in a way that facilitates using Lean's existing tactics. Finally, we provide examples illustrating the utility of the library in reasoning about systems that come from applications.