Abstract
統一化在自動定理證明中扮演一個不可或缺的角色。證明定理之速度和統一化的速度有直接關係。因此，找出一個高效率的統一化方法是十分有必要的。巳經有數個統一化方法被人提出來；但到目前為止，所提出的都是順序式計算方法。其中有些方法非常耗費時間，另外有些方法則不太容易施行。隨著硬體技術的進步，硬體設備愈來愈低廉，其能力也愈來愈強，記憶容量也一直地在加大。因此，多處理器系統巳是必然的趨勢。但無論硬體如何進步，一定要有好的計算方法才能使其達到最好的運作。在本論文中，我們將先提出一個可以用平行處理法來施行的統一化方法。接著證明該計算方法之正確性；同時，其複雜性也將加以分析。另外，我們將在平行隨取機器上來施行該計算方法。