A program for proving theorems stated in some formal logic.
Different theorem provers achieve different degree of automation.
One of the main applications of theorem provers is proving correctness of software and hardware computer systems (see formal methods).
Some popular theorem provers are: Isabelle, HOL, ACL2, Simplify, Otter, Vampire, Waldmeister, SPASS, Gandalf.