U.S.-France Cooperative Research: Rewriting and Rule- Completion Techniques for Horn Theories with Equality

该奖项将支持美国爱荷华大学计算机科学系张汉涛博士与美国爱荷华大学计算机科学系张汉涛博士的合作研究。Emmanuel Kounalis和Michael Rusinowitch，法国Nancy信息研究中心。该项目的目标是证明在逻辑编程中用于处理相等关系的良好技术。霍恩逻辑是一阶逻辑的一种限制，为计算机科学中的许多应用提供了最有用的逻辑基础，例如，专家系统、数据库系统、代数规范、逻辑编程和符号演算。在角逻辑的许多应用中，将相等关系引入到角逻辑中是很重要的。由于Horn子句将被解释为有条件的重写规则，并且将使用重写技术来处理相等关系，因此本项目研究者提出进行理论研究，研究不同的重写和完成技术。这项研究的结果将在一个名为RRL（重写规则实验室）的软件系统中实现，RRL是一个定理证明器，用于实验和开发基于重写方法的新的自动推理程序。RRL已经成功地用于解决通常被认为是机械化定理证明者的挑战的问题，包括在硬件和软件的验证和规范方面的重要应用。这个项目的重点是在RRL中实现一个类似prolog的解释器，并尝试不同的重写技术。进一步的研究也将在分析逻辑程序的结构性质的方法，如一致性，终止和定义完备性和计算在不完全指定的逻辑程序。该项目将受益于美国和法国研究人员在符号计算方面的互补专业知识。

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.