Redundance control is always considered as one of the most challenging problems to the automation of reasoning, because of combinatorial explosion in inferences generated during the search of solutions (of any non-trivial problems). This project will investigate a powerful inference rule called clausal superposition, which combines resolution and paramodulation together, but generates much less inferences. This project will also investigate a simplification rule called contextual rewriting, which identifies many unnecessary inferences and is more powerful than demodulation and subsumption together. The approach taken in this project is based on well-founded term orderings, which play a central role in the Knuth-Bendix completion procedure and rewriting methods for equational reasoning. In this project, results of theoretical investigation will also be implemented and experimented with in a software system called the Rewrite Rule Laboratory (RRL), an environment for experimenting with and developing new automated reasoning procedures based on rewrite methods. This research will increase the power of RRL for solving problems in verification and specification of hardware and software, as well as those considered a challenge for automated theorem provers.
