The problem of finding a strategy to control binary paramodulation

This article is the fifth of a series of articles discussing various open research problems in automated reasoning. Here we focus on the equality relation which is so vital to many applications of automated reasoning. The prolem proposed for research asks one to find a strategy for controlling the application of binary paramodulation. For evaluating a proposed solution to this research problem, we include suggestions concerning possible test problems.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.