Automated Planning Techniques for Elementary Proofs in Abstract Algebra

TL;DR

This paper demonstrates how automated planning techniques can be effectively applied to construct elementary proofs in abstract algebra, advancing automated theorem proving methods.

Contribution

It introduces a novel application of automated planning to elementary algebra proofs, bridging automated planning and theorem proving fields.

Findings

Automated planning techniques successfully construct elementary algebra proofs.

Implementation models implications and rules for commutative rings.

Initial results show promise for automated planning in theorem proving.

Abstract

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.