Research in Term Rewriting Systems and Automated Deduction,

术语重写系统和自动演绎研究，

• 批准号: 8802282
• 负责人: David Plaisted
• 金额: $ 16.08万
• 依托单位: University of North Carolina at Chapel Hill
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1988
• 资助国家: 美国
• 起止时间: 1988-12-15 至 1991-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=8802282&HistoricalAwards=false
• 关键词: Research; Term; Rewriting; Systems; Automated

It is proposed to investigate term rewriting systems and mechanical theoremproving strategies. The topics to be studied include: polynomial timealgorithms for reducing ground term rewriting systems to canonical form, andtheir application to the rigid E.unification problem; semantics and confluencetests for conditional term rewriting systems; and the use of rewriting andunification in programming languages. The research has potential applicationsin program verification and automated reasoning.

建议研究项重写系统和机械定理改进策略。研究的主题包括：将地项改写系统化为规范形式的多项式时间算法及其在刚性e统一问题中的应用；条件项改写系统的语义和聚合测试以及编程语言中重写和统一的使用。该研究在程序验证和自动推理方面具有潜在的应用前景。