Automated theorem proving, in a nutshell, is the combination of symbolic logic with syntactic algorithms. A formal proof calculus is chosen with two criteria in mind: expressiveness and ease of automation. These desiderata pull in opposite directions: Boolean logic and linear arithmetic are decidable, so the answers to all questions can simply be calculated, but these theories are not very expressive. At the other extreme, a dependent type theory such as the calculus of constructions used in Coq [6] is highly expressive and flexible, but complicates automation; even basic rewriting is difficult. Higher-order logic is often seen as a suitable compromise, expressive enough to reason directly about sets and functions, while still admitting substantial automation (especially in the case of Isabelle [18]).