Hyper-Linking with Equality and Semantics

子句链接定理证明方法最近被开发并在各种问题上进行了测试，包括集合论和时序逻辑中的问题，以及逻辑难题。该命题将一阶问题转化为命题演算，然后应用类似于Davis和Putnam方法的命题决策过程。这个项目将把这个定理证明方法扩展到涉及等式和项重写的问题。这涉及到像布兰德的修改方法这样的表示法与传统的术语重写技术的结合。一个解决涉及词典顺序路径排序的不等式的过程将被用来近似专门的统一算法。这项工作还将纳入有意义的语义来指导搜索；语义将作为计算结构中函数和谓词符号的意义的过程集合，以及确定结构中存在句的满意度的过程。将开发生成似是而非的引理并使用它们来指导寻找证据的方法。证明人将被应用于非平凡的数学定理。

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.