Instance-Based Theorem Proving with Semantics and Equality

基于实例的定理证明语义和等式

• 批准号: 9627316
• 负责人: David Plaisted
• 金额: $ 8.92万
• 依托单位: University of North Carolina at Chapel Hill
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1996
• 资助国家: 美国
• 起止时间: 1996-08-01 至 1998-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9627316&HistoricalAwards=false
• 关键词: Instance; Based; Theorem; Proving; Semantics

First-order logic is a common formalism for representing mathematical and other formal knowledge. Many traditional techniques for proving first-order theorems on a computer suffer from severe inefficiencies on certain kinds of problems such as near-propositional highly non-Horn problems. Under previous grants, theorem proving strategies have been developed that avoid many of these propositional inefficiencies. These include hyper- linking and hyper-linking with semantics. The latter method is able to make use of realistic models, or semantics, of the problem. However, the kinds of models it can use are limited to those involving linear inequalities and those with finite domains. This approach will now be extended to include a much more general class of models, those whose functions and predicates are computable. First-order logic with equality is a more powerful formalism that is also often applicable. For this formalism, methods based on term-rewriting systems are commonly applied. The above-mentioned semantic techniques will be extended to first-order logic with equality. Other topics related to equality will also be studied, such as rigid E-unification and specialized algorithms for handling permutations that arise from equational systems. A general framework---recently developed for studying the search efficiency of theorem proving strategies, and applied in a largely propositional context---will be extended to first-order logic. Complexity issues related to term-rewriting proofs will also be studied. ***

一阶逻辑是表示数学和其他形式知识的一种常见的形式主义。许多用于在计算机上证明一阶定理的传统技术在某些类型的问题上存在严重的低效，例如接近命题的高度非Horn问题。在以前的资助下，定理证明策略已经被开发出来，以避免许多这些命题效率低下的问题。这些链接包括超链接和带语义的超链接。后一种方法能够利用问题的真实模型或语义。然而，它可以使用的模型类型仅限于涉及线性不等式的模型和具有有限域的模型。这种方法现在将扩展到包括更一般的模型类，这些模型的函数和谓词是可计算的。具有等式的一阶逻辑是一种更强大的形式主义，也经常适用。对于这种形式主义，通常采用基于术语重写系统的方法。上述语义技术将扩展到一阶等价性逻辑。与等式相关的其他主题也将被研究，例如严格的E-统一和处理从方程系统产生的排列的专门算法。一个通用的框架-最近为研究定理证明策略的搜索效率而开发的，并主要应用于命题上下文-将被扩展到一阶逻辑。与术语重写证明相关的复杂性问题也将被研究。***