Proof-Producing Congruence Closure
Proof-Producing Congruence Closure
复制标题
证明产生的同余闭包
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Albert Oliveras
中科院分区：
文献类型：
--
作者：
R. Nieuwenhuis;Albert Oliveras
如今，许多一致性关闭的应用都需要在数千个输入方程中恢复的能力，即导致给定术语对等效的小子集。为此，在这里，我们引入了一种增量的一致性闭合算法，该算法具有额外的$ MATHIT {insell} $操作。
首先，引入了两种具有$ Mathit {Invell} $的Union-Find数据结构的变体。然后，将它们应用于与$ mathit {insplion} $的一致性关闭算法中，其中可以在几乎最佳的时间内恢复k-step的证明（k中的quasi linear，in k），而无需增加整体o（n log n log n）运行时最快的一致性关闭算法。
这种非平凡的（地面）方程推理结果已被广泛追求（例如，参见[SD99，DMRS04，KS04]），此外，还具有重要的应用程序。
Many applications of congruence closure nowadays require the ability of recovering, among the thousands of input equations, the small subset that caused the equivalence of a given pair of terms. For this purpose, here we introduce an incremental congruence closure algorithm that has an additional $mathit{Explain}$ operation.
First, two variations of union-find data structures with $mathit{Explain}$ are introduced. Then, these are applied inside a congruence closure algorithm with $mathit{Explain}$, where a k-step proof can be recovered in almost optimal time (quasi-linear in k), without increasing the overall O(n log n) runtime of the fastest known congruence closure algorithms.
This non-trivial (ground) equational reasoning result has been quite intensively sought after (see, e.g., [SD99,dMRS04,KS04]), and moreover has important applications to verification.