ResolutionPrinciple

こんな証明はできないのか

clauseの集合を {P(a), Q(a), Q(b)} としたとき any x. P(x) → Q(x) は証明できるのか? できないみたい。 Herbrand Universeで成り立っても、必ずしも成り立たないようなかんじ。 もしも、 {P(a), P(f(x))} で P(f(x)) の証明は当然できる。