The problem of choosing the type of subsumption to use

This article is the eighteenth of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find criteria for choosing the type of subsumption (if any) to use for completing a specific assignment. Since subsumption can be expensive (in terms of computer time), the application of such criteria to select the most effective variant of subsumption for attacking a specific problem might materially affect the liklihood of success. As possible test problems for evaluating a proposed solution to this research problem, we suggest SAM's lemma, theorems from Tarskian geometry, and theorems from equivalential calculus.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.