This award will support collaborative research between Dr. Hantao Zhang, Department of Computer Science, University of Iowa, and Drs. Emmanuel Kounalis and Michael Rusinowitch, Centre de Recherche en Informatique de Nancy (CRIN), France. The objective of the project is to justify good techniques to be used in Logic Programming for handling the equality relation. Horn Logic, a restriction of first order logic, has provided a most useful logical basis for many applications in computer science, for example, expert systems, database systems, algebraic specifications, logic programming, and symbolic calculus. In many applications of Horn Logic, it is important to incorporate the equality relation into the logic. Because Horn clauses will be interpreted as conditional rewrite rules and rewriting techniques will be used to handle the equality relation, the investigators in this project propose to carry out theoretical research to study different rewriting and completion techniques. The results of the study will be implemented in a software system called RRL (the Rewrite Rule Laboratory), a theorem prover for experimenting with and developing new automated reasoning procedures based on rewrite methods. 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. The focus of this project will be to implement in RRL a Prolog-like interpreter and to experiment with different rewriting techniques. Further investigations will also be conducted on methods for analyzing structural properties of logic programs, such as consistency, termination and definitional completeness and for computing in incompletely specified logic programs. The project will benefit from the complementary expertise of the US and French investigators in symbolic computation.
