NYI: High Performance Automated Reasoning and its Applications

NYI：高性能自动推理及其应用

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

9357851 Zhang Reasoning algorithms are used in many application areas of computer science and artificial intelligence, and high performance of reasoning algorithms is indispensable to the successes of these applications. The objectives of this research are to develop high performance reasoning algorithms, and to apply these algorithms in formal verification of hardware and software designs. This research will substantially improve the performance of a software system called RRL (Rewrite Rule Laboratory) by adding new reasoning algorithms into it, and by building new applications on the top of it. The research will focus on redundance control of automated deduction and mathematical induction, and efficient representation of data structures. The topics include restricted inference rules, powerful simplification rules, unnecessary computation detection, induction schemata formulation, induction hypotheses handling, and efficient implementations 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 world-wide to the people who are interested in using RRL as either a research tool or a teaching tool in automated reasoning. ***

9357851张推理算法在计算机科学和人工智能的许多应用领域都有应用，而这些应用的成功离不开推理算法的高性能。本研究的目标是开发高性能的推理算法，并将这些算法应用于硬件和软件设计的形式化验证。这项研究将通过在RRL（重写规则实验室）软件系统中添加新的推理算法，并在其基础上构建新的应用程序，从而大大提高RRL（重写规则实验室）的性能。研究的重点是自动演绎和数学归纳的冗余控制，以及数据结构的有效表示。主题包括限制推理规则、强大的简化规则、不必要的计算检测、归纳模式的制定、归纳假设的处理以及所有相关算法的有效实现。将从软件和硬件设计中选择实际验证问题作为RRL的测试问题，并通过提供抗故障和用户友好的界面来增强RRL以满足大规模应用的需要。我们将特别努力将RRL分发给全世界有兴趣使用RRL作为自动推理研究工具或教学工具的人。＊＊＊