The problem of hyperparamodulation and nuclei

This article is the thirty-third of a series of articles discussing various open research problems in automated reasoning. The problem for research asks one to establish criteria for allowing certain — but not all — new clauses to become nuclei when using the inference rule hyperparamodulation or hyperresolution.This work was supported by the Office of Scientific Computing, U.S. Department of Energy, under Contract W-31-109-Eng-38.