Acta Scientiarum Naturalium Universitatis SunYatseniVol. 26, Issue 3, Pages: 48-53(1987)
作者机构:
中山大学计算机科学系
作者简介:
基金信息:
DOI:
CLC:
Published:1987,
Published Online:25 May 1987,
扫 描 看 全 文
The Unification of AC Function. [J]. Acta Scientiarum Naturalium Universitatis SunYatseni 26(3):48-53(1987)
DOI:
The Unification of AC Function. [J]. Acta Scientiarum Naturalium Universitatis SunYatseni 26(3):48-53(1987)DOI:
The Unification of AC Function
摘要
本文考虑在自动定理证明中
一类特殊项的合一问题
给出一个简单的充分必要条件
用以判断满足结合律、交换律的两函数的可合一性
其时间复杂性几乎是线性的
且能较快地给出两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