High Performance Automated Reasoning

高性能自动推理

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

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.

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