Mathematical Sciences: Toward a Theory of Well-Founded Orderings for Use in Automated Deduction

数学科学：走向一种用于自动演绎的有根据的排序理论

• 批准号: 9510164
• 负责人: Patricia Johann
• 金额: $ 1.8万
• 依托单位: Hobart and William Smith Colleges
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1995
• 资助国家: 美国
• 起止时间: 1995-09-01 至 1997-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9510164&HistoricalAwards=false
• 关键词: Mathematical; Sciences; Toward; Theory; Well

9510164 Johann Well-founded orderings are ubiquitous in automated deduction, being fundamental to the development of termination proofs for computations in rewrite-based deduction systems, as well as of deduction strategies aiming to restrict search spaces in saturation processes. The determination of well-founded orderings suitable for a particular purpose, however, typically requires a good deal of technical expertise, and because termination of rewriting is undecidable in general the best that can be hoped for is to have a sufficient understanding of a sufficient variety of orderings to be able to cope with the many kinds of termination and efficiency problems which occur in practice. This research planning grant undertakes to develop a comprehensive theory of well-founded orderings based on their logical and numerical invariants. Two specific directions for further research are extending known results to larger classes of terms, and obtaining similar results for more general well- founded orderings, such as exponential orderings. As a further, related line of inquiry, a theory of nontotal well-founded orderings will be explored. Since the notion of order type makes no sense for nontotal orderings, appropriate logical invariants will need to be determined. ***

9510164 Johann 有根据的排序在自动演绎中无处不在，是基于重写的演绎系统中计算终止证明的开发的基础，也是旨在限制饱和过程中搜索空间的演绎策略的基础。 然而，确定适合特定目的的有根据的排序通常需要大量的技术专业知识，并且因为重写的终止通常是不可确定的，所以最好的希望是对足够的多样性有充分的理解的订单能够应对实践中出现的多种终止和效率问题。 这项研究计划拨款致力于根据其逻辑和数值不变量开发一种有充分依据的排序的综合理论。 进一步研究的两个具体方向是将已知结果扩展到更大的术语类别，并为更一般的有根据的排序（例如指数排序）获得类似的结果。作为进一步相关的探究，我们将探讨一种非完全有根据的排序理论。 由于订单类型的概念对于非全排序没有意义，因此需要确定适当的逻辑不变量。 ***