Completion for Multiple Reduction Orderings
Completion for Multiple Reduction Orderings
复制标题
完成多重降序
DOI：
--
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
Hisashi Kondo
中科院分区：
文献类型：
--
作者：
M. Kurihara;Hisashi Kondo
我们提出了一个完成过程（称为MKB），多个减少订单。给定方程和一组约简排序，该过程模拟由并行进程执行的计算，每个并行进程执行具有给定排序之一的标准完成过程（KB）。然而，为了提高效率，我们开发了新的推理规则，这些规则作用于称为节点的对象，节点是由一对s：t项组成的数据结构，这些项与信息相关联，以显示哪些进程包含规则s → t（或t → s），哪些进程包含方程s Particit。这个想法是基于这样的观察：在不同过程中做出的一些推理通常是密切相关的，因此我们可以设计推理规则，在单个操作中模拟这些推理。我们的实验表明，MKB是显着更有效的比天真的模拟KB程序的并行执行，当减少订单的数量是足够大的。我们还提出了一个扩展，这种技术的不失败完成多个减少订单，这是有用的自动推理，包括方程定理证明的各个领域。
We present a completion procedure (called MKB) that works for multiple reduction orderings. Given equations and a set of reduction orderings, the procedure simulates a computation performed by the parallel processes each of which executes the standard completion procedure (KB) with one of the given orderings. To gain efficiency, however, we develop new inference rules working on objects called nodes, which are data structures consisting of a pair s : t of terms associated with the information to show which processes contain the rule s → t (or t → s) and which processes contain the equation s ↔ t. The idea is based on the observation that some inferences made in different processes are often closely related, so we can design inference rules that simulate these inferences all in a single operation. Our experiments show that MKB is significantly more efficient than the naive simulation of parallel execution of KB procedures, when the number of reduction orderings is large enough. We also present an extension of this technique to the unfailing completion for multiple reduction orderings, which is useful in various areas of automated reasoning, including equational theorem proving.