# Questions tagged [unification]

The tag has no usage guidance.

26 questions
1answer
37 views

### most general unifier: can a variable be substituted to a variable and a function?

i was wondering: when doing most general unifiers(MGU), can a variable be substituted to a variable and to a function? examples that illustrates my question: 1)loves(girlfriend(x),x) , loves(y,y) 2)...
1answer
33 views

1answer
110 views

### How to unify a pair of atomic formulas?

Unify the pair of atomic formulas $p(a,x,f(g(y))),\ p(z,h(z,u),f(u))$. Attempt following the alogrithm described below. We have \begin{align} \begin{aligned} a &=z\\ x &=h(z,u)\\ f(g(y))&...
1answer
94 views

### First Order Logic Resolution

During Resolution, Can a skolemization constant be replaced by a function? For example: ∃X e(X)∧ g(X) After replacing with skolemization constant ...
1answer
101 views

### First Order Logic, help in Unification and substitution process

I'm trying to solve a few unification problems, but this one is a bit tricky to me. I have to demonstrate how to derive the first one starting from the second one. $\phi$ (c, f(c,h(M,e(c))) $\phi$ (...
1answer
76 views

### Can this given set be unified?

Assuming a,b,c are constant, and the rest are variables, what is the result of unification to the following sets? P(f(x,z),r,t) , P(w,f(g(w),h(t),b) The obvious solution would be to do the ...
1answer
188 views

### Using the unification algorithm to determine whether pairs of formulas are unifiable

I would like to use the unification algorithm to determine whether or not the following pairs of formulas are unifiable, and if so, find a most general unifier, showing all my working. Am I doing it ...
1answer
97 views

### Most General Unification of variables with the same function

I have to find the Most General Unifier of the following atomic sentences P(x1,G(x2,x3),x2,B) and P(G(H(A,x5),x2),x1,H(A,x4),x4) After using the Martelli-Montanari Algorithm I ended up on the ...
0answers
433 views

### Unusual most general unifier example

we're trying to unify the following: P(x,f(y)) and P(z,z) (where P is a binary predicate, f is a unary function and x,y,z are variables) Following the algorithm, I first include the following ...
1answer
49 views

### Unification of $P(x,x)$ and $P(a,b)$ [closed]

Why can we not unify $P(x,x)$ and $P(a,b)$? Don't the substitutions $a/x$ and $b/x$ provide unification?
0answers
51 views