Hyper-Linking with Equality and Semantics

具有平等性和语义的超链接

• 批准号: 9108904
• 负责人: David Plaisted
• 金额: $ 19.28万
• 依托单位: University of North Carolina at Chapel Hill
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1992
• 资助国家: 美国
• 起止时间: 1992-02-01 至 1995-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9108904&HistoricalAwards=false
• 关键词: Hyper; Linking; Equality; Semantics

The clause-linking theorem proving method was recently developed and tested on a wide variety of problems, including problems in set theory and temporal logic, and logic puzzles. This prover converts a first- order problem to the propositional calculus and then applies a propositional decision procedure similar to the Davis and Putnam method. This project will extend this theorem proving method to problems involving equality and term rewriting. This involves a combination of representations like Brand's modification method, with traditional term-rewriting techniques. A procedure to solve inequalities involving the lexicographic path ordering will be used to approximate specialized unification algorithms. This work will also incorporate meaningful semantics to guide the search; the semantics will be presented as a collection of procedures for computing the meanings of function and predicate symbols in a structure, as well as a procedure for deciding the satisfaction of existential sentences in the structure. Methods for generating plausible lemmas and using them to guide the search for a proof, will be developed. The prover will be applied to non-trivial mathematical theorems.

子句连接定理证明方法是最近发展起来的， 测试了各种各样的问题，包括集合论中的问题 时间逻辑和逻辑谜题。 这个证明器转换了第一个- 顺序问题的命题演算，然后应用一个 类似于戴维斯和普特南的命题决策程序 法 本项目将把这个定理证明方法扩展到 涉及等式和项重写的问题。 这涉及到一个 组合的表示，如品牌的修改方法， 传统的术语重写技术。 一个程序来解决 涉及字典路径排序的不等式将用于 近似专门的统一算法。 这项工作还将 结合有意义的语义来指导搜索;语义 将作为一个程序的集合， 结构中的功能和谓词符号的含义，以及 判定存在句满足的程序 结构。 生成合理引理的方法及其应用 以指导寻找一个证明，将被开发。 证明者将 应用于非平凡的数学定理。