Semantically-guided goal-sensitive theorem proving