本文提出了一种基于深度学习的方法，使用 Linear-time Temporal Logic 规约来修复 sequential circuits，并且使用多模态表示学习的分层 Transformer 模型来修复，并提出了一种数据生成算法用于扩展到更复杂的规约和 out-of-distribution 数据集。海量实验结果证明我们的方法可以显著提高基于 LTL 规约的自动化电路合成效果。

Mar, 2023

提出了一个基于给定句子算法的自动定理证明器的新的内部指导方法，该方法使用先前证明中的正负例影响未处理子句的选择。为此，提出了一种基于幺半群结构的类型广义标签出现次数的朴素贝叶斯分类的有效方案。将这种方法在高阶逻辑证明器 Satallax 中完成，证明了该方案比不具有内部指导的 Satallax 可以解决更多问题，能够扩展现有的快速分类器。在 Flyspeck 项目的一个简单类型的高阶逻辑版本上评估了我们的方法，在没有内部指导的 Satallax 不能解决的 26% 的问题上可以解决。

May, 2016

研究了描述逻辑 (DL) TBox 的表达能力，相对于一阶逻辑，基于诸如双仿、等仿、不交并和直积等语义概念，特征化了 AL、ALCQIO、DL-Lite 和 EL 等表达 DL TBoxes 的各种 DL。通过对于 DL TBox 可以被等价地重写为 L' 片段的 TBox 决策问题的首次研究，阐明了特征化的使用。

Apr, 2011

研究表明，将二进制和三进制变压器网络应用于大型语言模型能够显著减少内存并提高推理速度，并且研究结果显示，这些网络在学习模块化加法时与全精度变压器网络学习的算法相似，因此无法作为语言模型中更可解释的替代方案。

May, 2024

该论文提出了两种学习 Linear Temporal Logic（LTL）公式的新算法，该算法通过将学习任务简化为命题布尔逻辑中的一系列可满足问题来实现，并且验证了这两种算法在合成基准测试和领导者选举协议的执行理解方面的优异表现。

Jun, 2018

研究了如何构造多项式多个正负示例唯一确定的不变式查询，提出了前沿算法并讨论其在描述逻辑和模式映射中的应用。

Aug, 2020

本文总结了两种不同的问题设置中，从正面或反面的示例中学习 LTL 公式的两种方法，第一种方法假设示例标记有噪声，第二种方法则考虑在仅给出正面示例的情况下推断有意义的 LTL 公式，所提出的方法提供了解决上述问题的不同算法，以及推断时的其他时间性质描述，如信号时间逻辑或确定性有限自动机。

Dec, 2022

我们提出了一种基于图表示学习的模型检测框架，通过学习系统和规范的图结构表示，将模型检测问题转化为二分类问题，实验证明该方法在两种模型检测场景下取得了令人满意的准确性和速度提升。

Aug, 2023

本文探讨了神经符号计算中的两个基本问题：深度学习是否能够端到端地解决逻辑中的挑战性问题，以及神经网络是否能够学习逻辑的语义。研究重点是线性时间暂态逻辑（LTL），通过训练 Transformer 来直接预测给定 LTL 公式的解，使用传统求解器产生的经典解决方案生成训练数据，研究表明，使用这些特定的解决方案进行训练已足够。 Transformers 甚至可以预测在文献基准测试中，经典求解器超时的公式的解，它也可以推广到逻辑的语义，虽然与经典求解器找到的解有所不同，但仍可以正确地预测大多数公式的解。

Mar, 2020

通过分析命题线性时间逻辑 LTL 与 EL 或 ELI 描述逻辑中的概念结合的 2D 语言所查询的时间知识图中的路径形查询，研究了一些查询操作可以通过（多项式大小的）正 / 负时间数据示例的集合来唯一地描述的可能性，探讨了这些查询的多项式特性，并将其应用于活性学习框架中对时间实例查询的学习。

May, 2022