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