我到处寻找我能找到的关于这个主题的任何信息，但我找不到任何东西。甚至我的教科书也完全跳过了它。
关于统一 Skolem 功能甚至一般功能的规则是什么？
For example, can functions unify with constants?
Can R(f(x)) unify with R(A), where A is some constant?
Every example I've seen has been of the form R(f(x)) unifying with R(y)
or R(f(x) unifying with R(f(A)) which are all pretty obvious.
The example that really stumped me came from a solution to a resolution problem
in my Textbook, where they resolved the statement
Rel(Parent, P(x,y),x) ∧ Rel(Parent, P(x,y), y) ∧ x != y ⇒ Rel(Sibling,Me,y)
with
Rel(Parent, FM, Me)
to get
Rel(Parent,FM,y) ⇒ Me != y ⇒ Rel(Sibling,Me,y)
Where P(x,y) is a skolem function and FM is a skolem constant representing the
Father of Me
I understand the substitution of x = ME, but I don't understand how P(x,y)
unified with FM.
任何人都可以有所了解吗？