This paper explores the application of automated planning to automated theorem proving, which is a branch of automated reasoning concerned with the development of algorithms and computer programs to construct mathematical proofs. In particular, we investigate the use of planning to construct elementary proofs in abstract algebra, which provides a rigorous and axiomatic framework for studying algebraic structures such as groups, rings, fields, and modules. We implement basic implications, equalities, and rules in both deterministic and non-deterministic domains to model commutative rings and deduce elementary results about them. The success of this initial implementation suggests that the well-established techniques seen in automated planning are applicable to the relatively newer field of automated theorem proving. Likewise, automated theorem proving provides a new, challenging domain for automated planning.

翻译：本文探讨了自动化规划在自动定理证明中的应用，后者是自动化推理的一个分支，专注于开发用于构造数学证明的算法与计算机程序。具体而言，我们研究了如何利用规划技术在抽象代数中构造初等证明——抽象代数作为研究群、环、域和模等代数结构的严格公理化体系。我们在确定性与非确定性领域内实现了基本蕴含关系、等式及规则，以建模交换环并推导其基本结论。该初始实现的成功表明，自动化规划领域已成熟的技巧可应用于相对新兴的自动定理证明领域；与此同时，自动定理证明也为自动化规划提供了具有挑战性的全新领域。