Lemmatization in semantic strategies

I studied lemmaizing and caching techniques as a way of combining forward and backward reasoning in semantic resolution strategies. This approach allows one to understand lemmatization as a meta-level inference rule, and covers lemmatization in model elimination as a special case:

Maria Paola Bonacina and Jieh Hsiang. On semantic resolution with lemmaizing and contraction and a formal treatment of caching. New Generation Computing 16(2):163-200, February 1998; DOI: 10.1007/BF03037315.
Maria Paola Bonacina and Jieh Hsiang. On semantic resolution with lemmaizing and contraction. Proceedings of the Fourth Pacific Rim International Conference on AI (PRICAI), Springer, Lecture Notes in Artificial Intelligence 1114, 372-386, 1996; DOI: 10.1007/3-540-61532-6_32. (Part of this work was presented at the Dagstuhl Seminar 9512 on Deduction of March 1995 [Slides]).

Maria Paola Bonacina