AI 中文总结
研究面向miniKanren的有理项合一，基于Martelli-Rossi方法提出高效算法，性能与传统方法相当，还在Rocq证明助手提供算法属性认证证明及展示性能评估结果。
AI 中文摘要
我们提出了一种在持久设置中进行有理项合一的高效算法，与传统的用于Herbrand项的带三角替换的miniKanren合一相比，性能相当。该算法基于现有的Martelli-Rossi方法，并进行了一些调整以使实现更常规。我们在Rocq证明助手 中提供了主要算法属性的认证证明，并展示了全面性能评估的结果。
英文摘要
We present an efficient algorithm for rational term unification in persistent settings which demonstrates a comparable performance w.r.t. the conventional miniKanren unification with triangular substitution for Herbrand terms. Our algorithm is based on existing Martelli-Rossi approach and uses some adjustments to make the implementation more conventional. We provide certified proofs of principal algorithm properties in the Rocq proof assistant and showcase the results of a comprehensive performance evaluation.
