本文提出了一种新的问题转化方法，将 CNF 公式的决策问题转化为 Horn 公式的最大可满足性问题，并证明了在鸽笼公式的情况下 MaxSAT resolution steps 的数量存在多项式绑定。

May, 2017

通过对存在量化变量数量的参数化，我们开发了一种适用于有界子句长度的共价正常形式（CNF）QBF 实例的新型固定参数可解性算法。

May, 2024

该研究旨在解决将命题公式转化为任意格式的等价公式的问题，使用量子布尔公式编码的方法可以有效地解决此类问题，因为这种方法远优于使用暴力方法或者 SAT 求解器进行转化。

Mar, 2023

本文通过分析阐述了布尔可满足性问题中，采用了子句学习增强 DPLL 的实现方式是最高效的，并与已有的分辨规则证明体系相对照，证明了该方法在一些条件下可以提供更短的证明过程，且该算法可以通过利用问题结构，通过导向学习算法的方法取得指数性的加速。

Jun, 2011

本文采用量化布尔公式减少作为一种新的方法来展示固定参数线性算法，研究人工智能领域的几个已知问题，其中大部分问题已经通过使用 Courcelle 定理或动态规划证明了其固定参数线性，但作者认为采用 量化布尔公式 减少这种方法具有明显的优势。

May, 2018

本文介绍了一种新的 Answer Set Programming with Quantifiers ASP (Q) 的实现方式，它构建在 qasp 的基础上，具有更高效的编码过程和自动选择多个 QBF-solving 后端的算法选择策略，具有比 qasp 更好的性能表现。

May, 2023

开发了交互式定理证明器 Isabelle，以 Horn clause 表示每个推理规则，使用基于类型的 λ 演算表示逻辑语法，支持多个逻辑系统并具有逻辑编程潜能。

Oct, 2000

该研究提出一种名为 Manthan3 的数据驱动的方法，用于解决依赖量化布尔公式中的 Henkin 合成问题，实现对线路的验证、控制器合成和线路实现等应用方面具有积极的意义。

Jan, 2023

本研究介绍了面向棋盘游戏的领域定义语言（BDDL），并提供了一种有效的翻译方法，将 BDDL 转换为 QBF，以编码有界深度的胜利策略。我们使用 QBF 求解器计算了几个已知游戏的胜利策略关键深度，并展示了如何使用 QBF 证书和交互式游戏来验证胜利策略。

Mar, 2023

本研究展示了如何将命题演绎推广到受限伪命题逻辑（CPPL）中，这是将自然数与少量约束符号插入命题逻辑字母表并相应地调整底层语言所导致的扩展。虽然该限制被认为是不必要的，但本研究提供了一种建设性证明，证明了 CPPL 的广义演绎推理是正确而完整的。

Jun, 2023