该论文介绍了一个自动化推理系统 ACL2 定理证明器，其应用包括计算系统规范和验证，形式验证等，Boyer-Moore 家族的成员在 ACL2 Theorem Prover 研究和发展中做出重要贡献。
Sep, 2015
介绍了自 2011 年 ACL2 研讨会以来在 ACL2 版本中引入的增强功能，重点介绍了那些可以使用户受益的改进，但这些改进可能不会在日常实践中被发现。
Apr, 2013
本文介绍了自 2013 年 ACL2 研讨会以来对 ACL2 的改进，并涉及形式验证和定理证明方面的研究领域。
Jun, 2014
本文初步探讨了在 ACL2 系统上使用外部 ATP 进行实验的情况，旨在为解决 ACL2 问题提供外部推理和人工智能系统的初步效用评估。
该论文集收录了 ACL2 定理证明器及其应用方面的研究和经验，讨论 ACL2 定理证明器在技术论坛和应用方面的作用。
May, 2022
这篇论文介绍了一种名为 LRAT 的新型证明格式，它在 DRAT 基础上新增了 hints 以便于快速的验证算法，并可以使用定理证明器等已验证的系统来实现。作者还在 Coq 和 ACL2 中实现了两个经过认证的 LRAT 验证程序。
Dec, 2016
本文介绍一个名为 simplify-defun 的工具，它将给定函数的定义转换为新函数的简化定义，并通过 ACL2 提供证明，证明旧函数和新函数是等价的，并在适当时为新函数生成终止和守卫证明。该工具的工程结构使证明成功，并举例说明它在合成和验证中的实用性。
May, 2017
本文提出 IBR 模型，是一个迭代反向推理模型，用于解决基于规则的问答证明生成任务。IBR 通过迭代反向预测证明路径的节点和边缘，增强了推理过程的可解释性，同时利用节点和历史路径的详细表示进行推理，提高了推理的效率和准确性。实验结果表明，与强基线模型相比，IBR 具有更好的领域内性能和跨领域可迁移性。
本文开发了机器学习工具 ML4PG，并详细研究了在交互式定理证明器和使用电子库中的定理模式，以便为用户提供指导。
Jan, 2013
使用 Coq 深度嵌入 B 逻辑以检查其正确性和实现 B 工具，实现了 B 逻辑的证明器。
Feb, 2009