On Word Problems in Equational Theories
On Word Problems in Equational Theories
复制标题
论方程理论中的应用题
DOI：
10.1007/3-540-18088-5_6
复制
发表时间：
1987
期刊：
影响因子：
--
通讯作者：
M. Rusinowitch
中科院分区：
文献类型：
--
作者：
J. Hsiang;M. Rusinowitch
Knuth-Benzard程序在通用代数中的应用是非常有效的。然而，如果该过程生成不能被定向成规则的方程（即，该系统不是Noetherian的），或者如果它生成无限多的规则（即，系统不融合）。在1981年休特表明，即使系统是不融合的，克努特-Benidenth程序仍然会产生一个半决策程序字的问题，只要每一个方程可以定向。在本文中，我们表明，即使有些方程是不定向的，Knuth-Benzirt程序仍然可以修改成一个合理有效的半决策程序方程理论中的文字问题。因此，我们取消了Knuth-Benidorm程序中的诺特要求。几个汇合的结果，扩展和实验。完备性证明本身就是一个有趣的课题，它采用了一种新的证明技术，即利用超限语义树的概念来证明一般定理证明方法的反驳完备性。本文的内容如下：第1节简要介绍了项重写。在第二节中给出了可靠的Knuth-Benefit方法和汇流结果，并进行了一些讨论和比较。第3节将结果推广到一个更一般的理论，其中包括不等式。简化策略在第4节中给出。在第5节中，我们提出了完整性证明，以及一个定理证明策略的框架，它捕获了搜索计划的删除策略和公平性。第6节描述了一个具有一些实验结果的实现。部分包含了一些比较和讨论。本文报告的研究部分由美国国家科学基金会资助DCS-8401624和法国的Greco de Programmation支持。
The Knuth-Bendix procedure for word problems in universal algebra is known to be very effective when it is applicable. However, the procedure will fail if it generates equations which cannot be oriented into rules (i.e., the system is notnoetherian), or if it generates infinitely many rules (i.e., the system is notconfluent). In 1981 Huet showed that even if the system is not confluent, the Knuth-Bendix procedure still yields a semi-decision procedure for word problems, provided that every equation can be oriented. In this paper we show that even if some equations are not orientable, the Knuth-Bendix procedure can still be modified into a reasonably efficient semi-decision procedure for word problems in equational theories. Thus, we have lifted the noetherian requirement in the Knuth-Bendix procedure. Several confluence results, extensions, and experiments are given. So are some comparisons with related work.The proof of completeness, which is an interesting subject by itself, employs a new proof technique which utilizes a notion of transfinite semantic trees designed for proving refutational completeness of theorem proving methods in general.The outline of the paper is as follows: Section 1 briefly introduces term rewriting. The unfailing Knuth-Bendix procedure and confluence results are given in Section 2, together with some discussions and comparisons. Section 3 extends the results to a more general theory which includes inequalities. Simplification strategies are given in Section 4. In Section 5 we present the completeness proofs, as well as a framework of theorem proving strategies which captures the deletion strategies and fairness of search plans. Section 6 describes an implementation with some experimental results. Section contains some comparisons and discussions.Research reported in this paper is supported in part by the NSF grant DCS-8401624 and the Greco de Programmation of France.