High Performance Automated Reasoning

在过去的资助下开发的两个软件系统，RRL(重写规则实验室)SATO(满足性测试优化)，已经成功地用于解决许多通常被认为是自动定理证明器的挑战的问题，包括几十个拟群中的公开问题。本研究将进一步提高RRL和佐藤的推理能力。这项研究的目的是开发新的高性能推理算法，并将这些算法应用于硬件和软件的描述和验证，以及解决代数、逻辑和组合学中的公开问题。重点研究了约束满足和自动数学归纳法。这些主题包括有效的约束传播、并行和分布式推理、智能归纳模式的形成、大型证明的管理以及所有涉及的算法的实现和实验。将从软件和硬件设计验证和组合学中选择实际问题作为RRL和Sato的测试问题。这两个系统都将通过用户友好的界面进行改进，以满足大规模应用的需要。将作出特别努力，将RRL和佐藤分发给世界各地的自动推理社区。

Two software systems, RRL (the Rewrite Rule Laboratory) SATO (SAtisfiability Test Optimized), developed under the past grant, have been successfully used for solving many problems often considered a challenge for automated theorem provers, including several dozens of open problems in quasigroups. The current research will further increase the reasoning power of RRL and SATO. The objectives of this research are to develop new high performance reasoning algorithms, and to apply these algorithms in specification and verification of hardware and software, and in solving open problems in algebra, logic and combinatorics. The research focuses on constraint satisfaction and automated mathematical induction. The topics include efficient constraint propagation, parallel and distributed reasoning, intelligent induction schemata formulation, management of large proofs, and implementation and experimentation of all the involved algorithms. Practical problems will be chosen from software and hardware design verification and combinatorics as test problems for both RRL and SATO. Both systems will be enhanced to meet the need of large-scale applications by user-friendly interfaces. Special effort will be made to distribute RRL and SATO to the automated reasoning community worldwide.