I have trouble understanding MGU for functions, especially skolem functions.
Is it correct that in order to find MGU for 2 functions, say f(x) and g(y) then they must first of all be the same function ? f = g
I saw some solution comparing 2 skolem functions: R(x) = B(x) where R(x) describes the room x is in and B(x) describes the building x is in. The statements were: Visit(R(x)) and ~Visit(B(x)).
How could you possible unify 2 skolem functions if they are basically functions and functions are considered as constants in the sense that they can't be compared unless equal? I mean we have no knowledge that R = B so how can we state that R(x) = B(x) ?
You cannot unify $f(x)$ and $g(y)$.
We have a substitution, i.e. a finite set of the form $\{ t_1/v_1,\ldots,t_n/v_n \ \}$, where every $v_i$ is a variable, and every $t_i$ is a term.
A subst $\theta = \{ t_1/v_1,\ldots,t_n/v_n \ \}$ acts on an expression $E$ and $E \theta$ is the expression obtained from $E$ by replacing simultaneously each occurrence of the variable $v_i$ with term $t_i$.
A substitution $\theta$ is called a unifier for a set $\{ E_1,\ldots,E_k \}$ iff $E_1 \theta= E_2 \theta = \ldots = E_k \theta$. The set $\{ E_1,\ldots,E_k \}$ is said to be unifiable if there is a unifier for it.