NYI: High Performance Automated Reasoning and its Applications

9357851张推理算法被应用于计算机科学和人工智能的许多应用领域，而高性能的推理算法是这些应用成功不可或缺的一部分。本研究的目标是开发高性能的推理算法，并将这些算法应用于硬件和软件设计的形式化验证。这项研究将通过在RRL(重写规则实验室)中添加新的推理算法并在其上构建新的应用程序来显著提高RRL(重写规则实验室)的性能。研究的重点是自动演绎和数学归纳的冗余控制，以及数据结构的有效表示。这些主题包括受限的推理规则、强大的简化规则、不必要的计算检测、归纳模式的形成、归纳假设的处理以及所有涉及的算法的有效实现。实际验证问题将从软件和硬件设计中选择，因为RRL和RRL的测试问题将通过提供容错和用户友好的界面来增强，以满足大规模应用的需要。将特别努力在世界范围内向有兴趣将RRL用作自动推理的研究工具或教学工具的人分发RRL。***

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. ***