# Automated Theorem Prover

As opposed to proof assistants, there are also automated theorem provers. These are systems consisting of a set of well chosen decision procedures that allow formulas of a specific restricted format to be proved automatically. Automated theorem provers are powerful, but have limited expressivity, so there is no way to set-up a generic mathematical theory in such a system. [0]

[0] Geuvers, Herman. “Proof assistants: History, ideas and future.” Sadhana 34.1 (2009): 3-25.