A software system called RRL, the Rewrite Rule Laboratory, developed over the past four years with partial support from previous NSF grants, is both a theorem prover and an environment for experimenting with and developing new automated reasoning procedures based on rewrite methods. RRL includes implementations of a collection of rule-completion and rewriting algorithms that can be applied to proving predicate calculus and structural induction theorems. RRL has been successfully used for solving problems often considered a challenge for mechanized theorem provers, including significant applications in verification and specification of hardware and software. Further development of RRL and research in the associated theory are proposed. The focus will be to develop and extend RRL to be more useful and convenient for reasoning about software and hardware specifications and implementations. Towards this goal, RRL will be enhanced to provide powerful methods for automatically proving properties by induction. Theoretical research will be undertaken to combine two different approaches for automating proofs by induction, the proof by consistency approach and the explicit induction approach developed under the last NSF grant. Further investigations will also be conducted on methods for analyzing structural properties of specifications such as the consistency and definitional completeness properties and for reasoning about incomplete specifications. Theoretical and experimental research in developing heuristics, including identifying unnecessary computations, will be undertaken to improve the performance of completion procedures and of first-order theorem proving methods. Complexity studies and efficient implementations of primitive operations will also be continued and results will be incorporated into RRL.
