High Performance Automated Reasoning

推理算法被用于计算机科学和人工智能的许多应用领域。由于实际问题的高度复杂性，高性能的推理算法对于这些应用的成功是必不可少的。一个叫做RRL的软件系统，重写规则实验室，是在过去几年里在NSF的支持下开发的，已经成功地用于解决许多问题，这些问题通常被认为是自动化定理证明的挑战。该项目将进一步提高RRL的推理能力。本研究的目标是开发新的高性能推理算法，并将这些算法应用于硬件和软件的规范和验证。研究的重点是自动演绎和数学归纳法的冗余控制。主题包括限制推理规则、强大的简化规则、不必要的计算检测、归纳模式的制定、归纳假设的处理以及所有相关算法的有效实现。将从软件和硬件设计中选择实际验证问题作为RRL的测试问题，并通过提供抗故障和用户友好的界面来增强RRL以满足大规模应用的需要。我们将特别努力向全世界对自动推理感兴趣的人分发RRL。

Reasoning algorithms are used in many application areas of computer science and artificial intelligence. High performance of reasoning algorithms is indispensable to the successes of these applications, because of the high complexity of real problems. A software system called RRL, the Rewrite Rule Laboratory, developed over the past years with the NSF support has been successfully used for solving many problems often considered a challenge for automated theorem provers. This project will further increase the reasoning power of RRL. The objectives of this research will be to develop new high performance reasoning algorithms, and to apply these algorithms in specification and verification of hardware and software. The research will focus on redundance control of automated deduction and mathematical induction. The topics include restricted inference rules, powerful simplication rules, unnecessary computation detection, induction schemata formulation, induction hypotheses handling, and efficient implemenations of all the involved algorithms. Practical verification problems will be chosen from software and hardware design as test problems for RRL and RRL will be enhanced to meet the need of large-scale applications by providing failure-resistant and user-friendly interfaces. Special effort will be made on distributing RRL worldwide to the people interested in automated reasoning.