Two software systems, RRL (the Rewrite Rule Laboratory) SATO (SAtisfiability Test Optimized), developed under the past grant, have been successfully used for solving many problems often considered a challenge for automated theorem provers, including several dozens of open problems in quasigroups. The current research will further increase the reasoning power of RRL and SATO. The objectives of this research are to develop new high performance reasoning algorithms, and to apply these algorithms in specification and verification of hardware and software, and in solving open problems in algebra, logic and combinatorics. The research focuses on constraint satisfaction and automated mathematical induction. The topics include efficient constraint propagation, parallel and distributed reasoning, intelligent induction schemata formulation, management of large proofs, and implementation and experimentation of all the involved algorithms. Practical problems will be chosen from software and hardware design verification and combinatorics as test problems for both RRL and SATO. Both systems will be enhanced to meet the need of large-scale applications by user-friendly interfaces. Special effort will be made to distribute RRL and SATO to the automated reasoning community worldwide.
