本文介绍了通过改良变换法来解决逻辑程序终止性分析的限制的方法，并将其应用于 AProVE 终止证明器进行实验与评估。

Mar, 2008

文章介绍了 FP2 程序，这是一种支持无限扩展谓词及任意元数谓词，支持认真和怀疑的稳定模型推理，并可用于奇环问题的解决的新型逻辑编程范例。

Jul, 2010

这篇论文提出了规则受限和循环受限程序的新类别，通过更全局地分析术语如何从规则的主体传播到头部来克服目前方法的各种限制。

Dec, 2015

我们提出了一种新颖的算法，该算法合成初级编程课程的命令式程序，基于枚举程序合成和静态分析相结合的关键思想，我们的算法在平均6.6秒内能够解决基准问题。

Feb, 2017

本文详细研究了量化可布尔逻辑以及其存在量化和全称量化变量的相关应用，特别是在可解释人工智能方面的应用，提出了一种新的量化语义，并探讨了变量/文字与存在性/普遍性量化之间的相互作用。此外，我们还确定了一些布尔公式和电路类别，其中量化可以有效地完成。

Aug, 2021

本文介绍了一种将组合子术语表示为证明树的方法，并引入了基于参数化组合子术语定义的证明模式，实现了基于连接结构演算的特征的自动化一阶证明的实现和第一批实验结果。

Sep, 2022

我们在Coq证明助手中开发了在归纳构造计算（CIC）中的合成oracle可计算性和Turing约简的概念，并使用连续函数的顺序连续性来描述有效拓扑中基于连续函数的定义。

Jul, 2023

利用Lyra框架，引入Tool Correction和Conjecture Correction机制，以提高Large Language Models在形式证明领域中的效果，其中Tool Correction用于减轻幻觉，并改善证明的准确性，而Conjecture Correction用于通过与证明器的交互来细化形式证明中的猜想，并通过与环境的互动进行子目标调整。

Sep, 2023

该研究论文通过泛化之前的左角转换方法，支持半环加权产生规则，并提供了对可以移动的左角进行更精细控制的能力。该泛化的左角转换方法通过用右递归替换左递归，与猜测转换方法定义了等价的加权语言，同时在生成树结构上存在重要差异。除此之外，对GLCT、猜测转换和原始语法的输出之间的形式关系进行了几项技术结果的探讨，并在九种语言的语法中对GLCT的效率进行了实证研究。

Nov, 2023

提出了FVEL，一种与大型语言模型一起进行交互式形式验证的环境，通过将给定的代码转化为Isabelle并利用神经自动定理证明来进行验证，利用Isabelle中的规则和定理，通过FVELER数据集进行评估，结果表明FVEL可在SV-COMP中解决更多问题并减少证明错误。

Jun, 2024