>>181
関数型じゃないね。論理型。
項の「値」を求めてるわけじゃない。
定理を満足する変数の値の組（代入）を求めている。

両方を組み合わせた関数論理型ってのもあるけど。