The problem of demodulating across argument and literal boundaries

This article is the twenty-fourth of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find an appropriate theory for modulating across argument and across literal boundaries. Because demodulation has proved so useful—is most cases, even crucial—to automated reasoning, extending this concept to permit canonicalization to be applied at the predicate and at the clause and subclause levels merits exploration. For evaluating a proposed solution to this research problem, we suggest problems from mathematics, logic, program verification, database inquiry, and the world of puzzles.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.