Theorem proving strategies: a search-oriented taxonomy

There are several ways of classifying theorem-proving strategies. The primary classification key in this taxonomy is to distinguish between those strategies that work on a set of objects (e.g., clauses) and develop implicitly many proof attempts, and those strategies that work on one object at a time (e.g., a goal clause, or a tableau) and develop one proof attempt at a time, backtracking when the current proof attempt cannot be completed into a proof.