模等式理论的反统一实现
计算机科学中的逻辑
2017-09-05 v2 人工智能
摘要
我们提出了 Heinz (1995) 定义的 E-反统一（E-anti-unification）的一种实现，其中利用项的等价类的树文法描述来计算模等式理论的泛化。我们讨论了几项改进，包括 Heinz (1995) 提出的变量受限 E-反统一的高效实现，并给出了相关的运行时间数据。我们展示了其在多个领域的应用，包括等式归纳证明中的引理生成、智力测试、发散的 Knuth-Bendix 完备化、归纳假设的强化以及关于有限代数的理论形成。
引用
@article{arxiv.1404.0953,
title = {Implementing Anti-Unification Modulo Equational Theory},
author = {Jochen Burghardt and Birgit Heinz},
journal= {arXiv preprint arXiv:1404.0953},
year = {2017}
}
备注
113 pages; 57 figures