Theorem proving strategies: a search-oriented taxonomy