本文提出了一种基于 Satisfiability Modulo Theories 的 Linear Temporal Logic 语言 ——LTLf Modulo Theories，该语言具有高表现力，可用于数据感知过程和规划的模型检验。我们提供了一种基于 SMT 编码的单遍树状表格系统的 LTLfMT 的半决策过程，并在黑色可满足检查工具中实现。实验结果表明了该算法在新型基准测试上的可行性。

Apr, 2022

本文研究了线性时间逻辑模块理论在有限轨迹上的应用，其中命题使用一阶公式替代，并且可以比较不同时间点引用的一阶变量。我们提出了一种用于 LTLfMT 表格的完备且有效的修剪规则，该规则在满足有限内存的抽象语义条件的任何 LTLfMT 公式下，通过增加新规则可以保证表格也能终止。最重要的是，这种技术使我们能够建立关于 LTLfMT 的多个片段可满足性的新的可判定性结果，并对已知类别给出新的可判定性证明。

Jul, 2023

本文研究了最近由 Wang 等人提出的一阶逻辑采样问题 —— 如何在有限域上高效地采样给定一阶句子的模型？我们将他们对于双变量逻辑 FO^2 的普遍量化子片段 UFO^2 的结果扩展到整个 FO^2 片段。具体来说，我们证明了 FO^2 在采样下的域可扩展性，即存在一种能在域大小多项式时间下运行的 FO^2 采样算法。然后，我们进一步表明，即使存在像所有 x 存在 = ky: φ（x，y）和存在 = kx 为所有 y 的数量约束，如 φ（x，y）的量化器公式，我们的方法也可以保持运作。我们的提出的方法是具有建设性的，由此产生的采样算法在各个领域都有潜在的应用，包括在组合结构和统计关系模型的均匀生成方面以及如 Markov 逻辑网络和概率逻辑程序的采样方面。

Feb, 2023

该报告介绍和正式说明了几个模态逻辑的标准主题，如标准模态公理之间的关系、可达性关系的属性、以及 Barcan 公式在常量和可变域中的属性，并提供了有效的自动化方法，将命题和量化模态逻辑嵌入到了 PVS 验证系统中。

May, 2022

该研究探讨了一个版本的线性时态逻辑，其命题片段是 Godel-Dummett 逻辑，并使用了两种自然语义学，一种是真值语义学，另一种是双关系语义学，证明了这些语义定义了相同的逻辑，并提出了决定语句有效性的算法以及一个用于 Godel 临时逻辑的演绎演算法，从而证明了所有的有效语句都能够用这个演算法证明。

Jun, 2023

该论文提出了一种包含线性不等式中计数模态的模态逻辑，证明了每个公式可以转化为等价的图神经网络（GNN），也证明了每个 GNN 可以转化为公式，说明可满足性问题是可判定的，并讨论了一些 PSPACE 内的变种。

Jul, 2023

论文探讨了一维统一片段（U1）的性质，以及 U1 与适应更高元关系的描述逻辑（DLR_reg）的关系，并定义了一个描述逻辑版本的 U1 变体，并证明了与 U1 和其他相关逻辑的表现力有关的一系列新结果。

Apr, 2016

本文研究了带有基数约束的分级模态逻辑在几个已知框架类别下的可满足性复杂度及其判定问题，并获得了紧密的复杂度界限，尤其是针对具有传递性框架的情况下缺乏树型模型性质的问题。

May, 2009

研究发现：在包含任意数量的传递关系的一元否定分段中，有限可满足性问题是可判定和 2-ExpTime 完全问题。此外，我们探讨了我们的基本逻辑的各种扩展的有限可满足性，特别是描述逻辑中已知的名称和角色层次概念的表达。

Sep, 2018

该论文涉及描述逻辑的特性，首次引入普遍量化的概念，提出两种扩展的语义模型，包括模态逻辑中的公理原型和二阶逻辑中的量词的替代。研究表明，在某些扩展的语义中，所得出的结论与经典的描述逻辑相符，并证明了某种程度上用于这种扩展的算法的多项式可判定性。

Aug, 2023