加权路径序的可验证高效实现
摘要：Yamada加权路径序（WPO）的证明终止性的强大技术及其与检查不可信终止性证明的CeTA的支持。更准确地说，CeTA包含一个经过验证的函数，用于计算给定WPO的两个项是否有一个大于另一个，即WPO的所有参数都已被固定。该经过验证的函数的问题在于其在最坏情况下的指数时间复杂度。 因此，在这项工作中，我们开发了一个基于记忆化的WPO多项式时间实现。它还改进了先前的递归路径顺序（RPO）实现：RPO实现使用完整的术语作为内存的键，这种设计简化了完备性证明，但有一定的运行时开销。在这项工作中，键只是数字，因此内存中的查找更快。尽管在纸上是平凡的，但这种变化给验证任务带来了一些挑战。
作者：Ren''e Thiemann and Elias Wenninger
论文ID：2307.14671
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-28