自動定理証明やプログラム合成のための有用な理論として高階単一化がある。 高階単一化は、１階の単一化とは異なり、関数も扱えるという点が有利である。 しかしながら、高階単一化は複雑で大変難しい問題であり、これまでにいくつ かの研究がなされているだけである。高階単一化は、一般には決定不能である ため、決定可能となるクラスについて研究が進められており、Prehoferらによっ て、線形２階パターンの単一化の決定性と、単一化アルゴリズムが示された。 本研究では、Prehoferの手法に基づいて、線形２階パターンの単一化実行系を 構築し、その性能を評価する。