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