The problem of demodulation during inference rule application

This article is the twenty-second of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find criteria for deciding when to permit and when to avoid demodulation during the application of inference rules, focusing mainly on hyperresolution, UR-resolution, and hyperparamodulation. Since these three inference rules admit natural points at which one or more demodulators (rewrite rules) could be applied-for example, after the removal of a literal or the replacement of a term-and since the dominant practice is to demodulate only after an inference rule has been completely applied, the proposed research focuses on an intriguing alternative. For evaluating a proposed solution to this research problem, we suggest problems from mathematics, logic, circuit design, program verification, and the world of puzzles.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Eneregy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

The problem of strategy and hyperresolution

This article is the thirty-first of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to find a strategy that can be coupled with the inference rule hyperresolution to control the behavior of an automated reasoning program as effectively as does paramodulation.This work was supported by the Office of Scientific Computing, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

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.     

Some Techniques for Proving Termination of the Hyperresolution Calculus

We define a semantic criterion ensuring termination of the hyperresolution calculus, which allows us to prove the decidability of certain classes of clause sets. We also define an algorithm for deciding – in polynomial time – whether a given clause set satisfies the proposed criterion. Comparisons with existing works on hyperresolution-based decision procedures are provided, showing evidence of the interest of our approach.     

The problem of explaining the disparate performance of hyperresolution and paramodulation

This article is the sixth of a series of articles discussing various open research problems in automated reasoning. Here we focus on the effectiveness of hyperresolution versus that of paramodulation. The problem proposed for research asks one to find the properties that explain why paramodulation is so much more effective than hyperresolution is for solving various problems from algebra. Fore 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.