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