计算性与图灵约简在归纳构造演算中的应用
本文探讨了“离散有限程序”和“有限递归程序”在“稳定模型语义”的语境下的性质，证明了“有限递归程序”的“一致性检查”和“怀疑推理”是“半可判的”，而“怀疑推理”对于“一般有限递归程序”具有完备性，并展示了如何使用有限的程序实例子集进行矛盾检查和响应怀疑查询。
Jan, 2009
介绍了一种概率类型的自然推导演算法，能够推导出概率计算过程的可信性，并通过对频率和预期概率之间的距离进行假设检验来形式化信任。该演算法在验证自动分类算法方面有潜在应用。
Jun, 2022
本研究介绍了一种基于Universal Transformer体系结构的语义解析方法，可以将基本数学证明转化为Coq互动定理证明器中的等效形式，以及将装饰有Hoare三元组的简单命令式代码翻译成Coq中的形式验证证明。通过人工和人工写作证明的有限领域的实验表明，这些模型对于训练期间未看到的中间长度和自然语言变化具有很好的泛化能力。
Jan, 2023
提出了一个通用的查询决策框架，基于计数模型的结构简单性，可以确定各种逻辑蕴涵问题（简称查询）的可决性，其中Blumensath的分区宽度作为一个特别强大的宽度度量提出，重点介绍存在规则的形式化，其中分区宽度的规则子域覆盖范式为一周围侧子域。
Apr, 2023
介绍了一种基于PDL的表达力丰富的逻辑家族CPDL+，研究了其最小模型检查问题和可满足性问题，将CPDL+的表达能力与树宽相关联，并通过基于树宽的逐步升级证明了其表达能力的严格上升。
Apr, 2023
介绍了 DHOL 的依赖类型扩展是如何保留了 HOL 的风格和概念框架，并且使用 DHOL 定理证明器实现了从 DHOL 到 HOL 的翻译，进而获得 DHOL 的定理证明器。
May, 2023
本文主要探讨了知识表示中重要的可决定性工具——Chase算法与证明理论中的证明搜索算法之间的联系，特别是在一阶逻辑的Gentzen序列演算的推广中探究了在存在性规则的情况下Chase机制本质上与证明搜索相同，并通过证明搜索生成知识库的通用模型，该特征也与Chase算法相同。
Jun, 2023
本研究通过对克雷格插值的输入和输出进行限制，并结合一阶 ATP 推导系统的子句平板验证方法，证明了在一阶逻辑中可以传递范围限制和 Horn 属性。同时，我们还展现了一种解决限制子句平板结构一般问题的方法，并将其应用于查询综合和插值重构。该方法结合了证明结构操作和高度优化的一阶推理器，具有可行的实现前景。
Jun, 2023
本文研究了线性时间逻辑模块理论在有限轨迹上的应用，其中命题使用一阶公式替代，并且可以比较不同时间点引用的一阶变量。我们提出了一种用于LTLfMT表格的完备且有效的修剪规则，该规则在满足有限内存的抽象语义条件的任何LTLfMT公式下，通过增加新规则可以保证表格也能终止。最重要的是，这种技术使我们能够建立关于LTLfMT的多个片段可满足性的新的可判定性结果，并对已知类别给出新的可判定性证明。
Jul, 2023