述語の分析(20190721)

例えば、-Pにつながるheadが{-P(t_1),-P(t_2),...}だったとする。 resolutionではこれらの間のresolutionは行わないが、canonical P(X)とこれらをunify()したmguを σ_1,σ_2,...としたとき、このclause set(axiom)が+Pリテラルを消す可能性のすべてがここにある。

[-P] = Π σ_i

でとらえられるのではないか??

変化するaxiomの場合はcheapthoughtで検討中。 [-P]ではとらえられない。

H^n の束構造の集合を[±P]が決めている clauseの構造はloopとか分岐か。constraintになっている。同じ±Pを含むと、大きな構造に影響受けるのか