On semantic resolution with lemmaizing and contraction and a formal treatment of caching