Automated theorem provers are programs that determine logical consequences of sets of statements. Interactive ATPs are commonly called “proof assistants”.
An Overview of Automated Theorem Proving
cvc5: Open source SMT solver from Stanford/UIowa
Logictools: Interactive predicate logic solver, good intro docs
Z3: Open source SMT solver from Microsoft