Redundancy Control in Automated Resasoning & Enhancement of the Rewrite Rule Laboratory

冗余控制一直被认为是最具挑战性的问题之一 问题的自动化推理，因为组合 在搜索解决方案的过程中产生的推理爆炸（ 任何不平凡的问题）。 该项目将调查一个强大的 推理规则称为子句叠加，它结合了解决方案 和调节在一起，但产生的推论要少得多。 这 该项目还将研究一种称为上下文的简化规则 重写，它识别了许多不必要的推论， 比解调和包容加起来还要强大。 的方法 在这个项目中采取的是基于良好的长期排序， 在Knuth-Benchmark完井程序中发挥核心作用， 等式推理的重写方法。 在这个项目中，理论研究的结果也将 在一个名为 重写规则实验室（RRL），一个实验环境， 开发新的基于重写的自动推理程序， 方法.该研究将提高RRL解决问题的能力 硬件和软件的验证和规范方面的问题， 以及那些被认为是对自动定理证明器的挑战。

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.