High Performance Automated Reasoning

两个软件系统，RRL（重写规则实验室） SATO（满意度测试优化），根据 过去的赠款，已成功地用于解决许多问题，往往被认为是 自动定理证明器的挑战，包括几十个开放的 拟群中的问题 目前的研究将进一步增加 RRL和SATO的推理能力。 本研究的目的是 开发新的高性能推理算法，并应用这些算法 硬件和软件规范和验证中的算法，以及 解决代数、逻辑和组合学中的开放性问题。研究 专注于约束满足和自动数学 诱导 主题包括有效的约束传播，并行和 分布式推理，智能归纳模式，管理 大量的证据，以及所有涉及的实施和实验， 算法 从软件和硬件设计中选择实际问题 验证和组合学作为RRL和SATO的测试问题。 两 我们会加强系统，以配合大规模应用的需要， 用户友好的界面。 将作出特别努力， 将RRL和SATO分发给全世界的自动推理社区。

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.