Rewrite Systems

重写系统

• 批准号: 9024271
• 负责人: Nachum Dershowitz
• 金额: $ 19.94万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1991
• 资助国家: 美国
• 起止时间: 1991-05-15 至 1994-10-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9024271&HistoricalAwards=false
• 关键词: Rewrite; Systems

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.

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