The Unification of AC Function[J]. Acta Scientiarum Naturalium Universitatis SunYatseni, 1987,26(3):48-53.DOI:
关于AC函数的合一问题
摘要
本文考虑在自动定理证明中
一类特殊项的合一问题
给出一个简单的充分必要条件
用以判断满足结合律、交换律的两函数的可合一性
其时间复杂性几乎是线性的
且能较快地给出两AC函数的一个合一式.同样
此法可推广使用.
Abstract
This paper is about a special kind of unification problem in automatic theorem proving. that is
the items are the function satisfying associative and commutative laws
shortly
AC function. A simple sufficient and necessary condition is given to decide whether two AC functions can be unified. The time complexity is almost linear. And a unifier for two AC functions can be derived quickly. Also