Rewrite Systems

本项目的目标是发展理论和应用 的重写。 Knuth-Benchmark完成程序最初是 旨在作为一种手段，采取公理化的方程 理论，并生成一个重写系统，可以用来决定 一个给定的方程是否从其他方程中得出。 完成还可以 当它产生无限重写时， 系统 这项工作将扩展推理规则和证明- 标准化的方法制定的完成，以产生 条件重写系统和谓词演算中的定理证明 与平等。 在更实际的方面， 条件重写将被探讨，因为它适用于功能 和逻辑编程范例，以及验证 将开发程序正确性方面。

The object of this project is to develop the theory and applications of rewriting. The Knuth-Bendix completion procedure was originally intended as a means of taking an axiomatization of an equational theory and generating a rewrite system that can be used to decide whether a given equation follows from the others. Completion may also be used as a theorem-prover when it generates an infinite rewrite system. This work will extend the inference-rule and proof- normalization approach developed for completion to the generation of condition rewrite systems and to theorem proving in predicate calculus with equality. On the more practical side, the semantics of conditional rewriting will be explored as it applies to the functional and logic programming paradigms, and useful techniques for verifying aspects of program correctness will be developed.