句子表格法进行范围受限插值
本文通过分析阐述了布尔可满足性问题中，采用了子句学习增强DPLL的实现方式是最高效的，并与已有的分辨规则证明体系相对照，证明了该方法在一些条件下可以提供更短的证明过程，且该算法可以通过利用问题结构，通过导向学习算法的方法取得指数性的加速。
Jun, 2011
本研究介绍了反证完成的超位置演算法，用于意图性和外延句子$\lambda$-自由高阶逻辑，这两种形式允许部分应用和应用变量。 这些演算法由一个术语排序参数化，无需完全单调，从而可以采用$\lambda$-自由高阶词典路径和Knuth-Bendix排序。作者们在Zipperposition prover中实现了这些演算法，并在Isabelle/HOL和TPTP基准测试中评估它们。 它们似乎是通向完全高效自动定理证明程序的一个重要的步骤。
May, 2020
该论文介绍一种名为 Standpoint logic 的多透视角逻辑推理方法，并提出了一种基于嵌套序列演算的证明系统，利用多重颜色技术实现最坏情况复杂性最优的证明搜索算法。
May, 2022
CD Tools是一个使用证明结构为中心的形式化视图来实践压缩分离的Prolog库，其中包括基于证明结构枚举的专门证明器，其中SGCD具有特别灵活的混合证明搜索方式，并在实验中显示了该方法的特征和应用潜力。
Jul, 2022
应用高阶自动推理证明器探索 Boolos' Curious 推论，通过提供适当的简写符号以发现短证明所需的高阶引理，并提出全证明自动化的可能性。
Aug, 2022
该研究旨在通过定义解释性、逻辑和公式大小来解决特定的解释问题，对命题逻辑进行了研究，最终提供了与n皇后和支配集问题相关的问题解释能力的实现。
Sep, 2022
本文介绍了一种将组合子术语表示为证明树的方法，并引入了基于参数化组合子术语定义的证明模式，实现了基于连接结构演算的特征的自动化一阶证明的实现和第一批实验结果。
Sep, 2022
介绍了 DHOL 的依赖类型扩展是如何保留了 HOL 的风格和概念框架，并且使用 DHOL 定理证明器实现了从 DHOL 到 HOL 的翻译，进而获得 DHOL 的定理证明器。
May, 2023
我们在Coq证明助手中开发了在归纳构造计算（CIC）中的合成oracle可计算性和Turing约简的概念，并使用连续函数的顺序连续性来描述有效拓扑中基于连续函数的定义。
Jul, 2023
本文研究了线性时间逻辑模块理论在有限轨迹上的应用，其中命题使用一阶公式替代，并且可以比较不同时间点引用的一阶变量。我们提出了一种用于LTLfMT表格的完备且有效的修剪规则，该规则在满足有限内存的抽象语义条件的任何LTLfMT公式下，通过增加新规则可以保证表格也能终止。最重要的是，这种技术使我们能够建立关于LTLfMT的多个片段可满足性的新的可判定性结果，并对已知类别给出新的可判定性证明。
Jul, 2023