Automated Planning Techniques for Elementary Proofs in Abstract Algebra
This work addresses the challenge of automated theorem proving for abstract algebra, but it is incremental as it builds on existing planning methods.
The paper tackled the problem of constructing elementary proofs in abstract algebra by applying automated planning techniques, resulting in an implementation that successfully modeled commutative rings and deduced results, suggesting cross-applicability between automated planning and theorem proving.
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.