Automated theorem provers are programs that determine logical consequences of sets of statements.
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