High Performance Automated Reasoning

高性能自动推理

• 批准号: 9504205
• 负责人: Hantao Zhang
• 金额: $ 18.76万
• 依托单位: University of Iowa
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1995
• 资助国家: 美国
• 起止时间: 1995-09-01 至 1999-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9504205&HistoricalAwards=false
• 关键词: Performance; Automated; Reasoning

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.

两个软件系统，RRL（重写规则实验室）SATO（可满足性测试优化），在过去的拨款下开发，已经成功地用于解决许多问题，这些问题通常被认为是对自动定理证明者的挑战，包括准群中的几十个开放问题。目前的研究将进一步提高RRL和SATO的推理能力。本研究的目标是开发新的高性能推理算法，并将这些算法应用于硬件和软件的规范和验证，以及解决代数、逻辑和组合学中的开放问题。研究的重点是约束满足和自动数学归纳法。主题包括有效的约束传播，并行和分布式推理，智能归纳模式制定，大型证明的管理，以及所有相关算法的实现和实验。从软件和硬件设计验证和组合学中选择实际问题作为RRL和SATO的测试问题。这两个系统将会得到加强，以方便使用者使用的介面，满足大规模应用的需要。将作出特别努力，向全世界的自动推理社区分发RRL和SATO。