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

该奖项将支持博士之间的合作研究。 Hantao Zhang，University of Technology计算机科学系 爱荷华州，以及伊曼纽尔·库纳里斯和迈克尔·鲁西诺维奇博士， Centre de Recherche en Informatique de Nancy（CRIN），France. 该项目的目标是证明良好的技术， 在逻辑程序设计中用于处理等式 关系。 Horn逻辑是一阶逻辑的一种限制， 计算机中许多应用程序的最有用的逻辑基础 科学，例如，专家系统，数据库系统， 代数规范、逻辑编程和符号 微积分在Horn逻辑的许多应用中， 将等式关系纳入逻辑。因为 Horn子句将被解释为条件重写 规则和重写技术将用于处理 平等关系，本项目的研究人员提出， 开展理论研究，研究不同的改写方式 完成技术。 研究结果将是 在一个称为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.