On Semantic Resolution with Lemmaizing and Contraction and a Formal Treatment of Caching