OVERLAPPING UNIFICATION ALGORITHM AND ITS HARDWARE IMPLEMENTATION.

[[abstract]]Unification is introduced as the basic operation in the inference-rule-of-resolution principle in first-order logic. In fact, unification must be performed at every inference step, and thus the efficiency of this operation affects crucially the performance of the whole theorem-proving process. An overlapping algorithm that is based on the original unification algorithm is proposed. By overlapping it is meant that some of the operations in the algorithm can be executed in parallel. This algorithm is simple and suitable for hardware implementation. An architecture for elegant execution of the algorithm is presented, and its performance is discussed.[[fileno]]2030201030029[[department]]資訊工程學