  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.
