I have heard about this topic, and I'm merely looking for a reference that I can read through: I know about formal logic as a proof-checking system, but I haven't yet learned about actual algorithms for automated theorem construction (except for the obvious naive algorithms, such as listing all possible proofs in lexicographic order and proof-checking each of them).
I'm looking for an introduction into the basics of this, specifically when it comes to equational reasoning, i.e. you have a number of equational axioms and need to prove another equation from it (e.g. the basic exercises one would do in group theory). I assume there must be a basic simple but reasonably efficient algorithm for this that is well-known