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）有充分根据自动扣除额无处不在，这对于开发基于重写的扣除系统中计算的终止证明以及旨在限制饱和流程中搜索空间的推论策略至关重要。 但是，确定适合特定目的的有良好的订单，通常需要大量的技术专业知识，并且由于终止重写是不可确定的，因此可以希望的最好的是对有足够的订单有足够的了解，以便能够应对许多在实践中发生的终止和效率问题。 这项研究计划赠款承诺根据其逻辑和数字不变性制定有良好的订单的全面理论。 进一步研究的两个具体方向将已知结果扩展到较大的术语，并为更普遍的良好基础订购（例如指数顺序）获得相似的结果。另外，将探讨相关的探究线，关于非功能良好的订单理论。 由于订单类型的概念对于非命令毫无意义，因此需要确定适当的逻辑不变性。 ***