# Questions tagged [unification]

The tag has no usage guidance.

37 questions
Filter by
Sorted by
Tagged with
21 views

### Can we unify 3 different First Order Logic sets/expressions?

Wherever I searched about unification in first-order logic (FOL) expressions, I could only find it as the unification of "two different logical atomic expressions identical by finding a ...
11 views

### Find the most general unifier

I have two terms: $(t_{2} \rightarrow (t_{1} \rightarrow (t_{0} \rightarrow t_{3})))$ and $(((Int \rightarrow t_{0}) \rightarrow t_{1}) \rightarrow t_{2})$ The task is to find the most general ...
• 101
1 vote
136 views

### Unification in first order logic

I know unification problem in first order logic is defined as a equation $t_1=s_1, ..., t_n=s_n$. My question is that why unification in first order logic can not be defined as a unification of a ...
• 31
67 views

### Is it possible to use Unification for lambda calculus?

Unification is an algorithmic process of solving equations between symbolic expressions. I have solved a few execercises in FOL: ...
• 415
122 views

167 views

### Unification of an expression : Example

Trying to learn Unification process, and while reading in a website about it, i found this example. Find the MGU of {p(f(a), g(Y)) and p(X, X)} ...
1 vote
38 views

### No most general unifier?

I have the task to find a most general unifier of these 2 terms: f(x, f(g(x),y)) f(g(y), f(g(z),z)) I applied the unification algorithm until almost everything was ...
• 11
1 vote
53 views

### Most general unifier - "infinite loop" - failure?

Lets say I have the following expressions where $x,y$ are both variables: $p(x,y)$ $p(y,x)$ Is there a most general unifier in this case? since $x,y$ are both variables do I get stuck in an ...
• 915
291 views

### First order logic: unification of Skolem constants?

My professor asks us to either prove a logical consequence by resolution or disprove it by giving a suitable interpretation. While doing one of the tasks, I encountered a problem with skolemization. ...
101 views

### Why is factoring causing wrong answer in resolution logic?

When performing resolution for the following KB: 1. Game(x) ^ Game(y) ^ Loves(z,x) => Loves(z,y) 2. Game(ResidentEvil) 3. Game(GodofWar) 4. Loves(John,GodofWar) ...
• 101
77 views

171 views

### Did Lie Theory manage to unify ordinary differential equations

In Lie Gourp wikipedia entry (https://en.wikipedia.org/wiki/Lie_group) it is said: The initial application that Lie had in mind was to the theory of differential equations. On the model of Galois ...
• 31
1 vote
523 views

### Show by Resolution that a set of clauses is unsatisfiable

Im trying to show by resolution that the following set of clauses is unsatisfiable: $\{ p(x,f(y)) \lor p(c,z), ¬p(y,f(f(y))) \lor ¬p(c,x) \}$. Now, I know that to show the unsatisfiability I need ...
453 views

### Most general unifier for set of equations?

Find the MGU in the following set of expressions $bar(1,Y,X,Y),bar(X,X,1,Z),bar(1,g(Y),1,f(W))$ Attempt I do not know if you can work with the 3 functions at the same time. So I did for 2 functions ...
278 views

1 vote
819 views

### Is the following a unifier, but not a most general unifier?

So I have the following pair of terms $p(q(A),r(A))$ and $p(q(A),r(B))$ I understand the most general unifier for this would be $B/A$. i.e. replace $B$ with $A$. But I am also aware that there is ...
• 543
3k views

### Most General Unifier computation

I'm trying to compute a most general unifier. There are many rules and I'm confused by them. So here is the example: {P(z,g(c)),P(g(x),z),P(z,z),P(g(y),g(c))} - ...
• 271
638 views

### The Most General Unifier

I am studing for logic and i need to unify these formulas: $$P(\;\; f(x,g(x,y))\;\; ,\;\; h(z,y)\; )$$ $$P(\;\; z \;,\; h(f(u,v),f(a,b))\; )$$ Can someone explain me what i need to do? I must ...
83 views

### Unification in languages without function symbols or with relational terms.

In case a logic formula is mechanically constructed, obtained as the specification of an expression in an imperative programming language for example, the functional constraints could be implicit in ...
• 163
2k views

### Associative, commutative properties and identity elements of non-binary functions

I'm making a compiler (for a new language) wich supports AC unification via pattern matching. The matching algorithms already works but i'm having trouble with the logical and mathematical aspects of ...
• 133
6k views

### Substitution To Find Most General Unifier

Could someone give me some advice on how to do this problem? For the the following pair of expressions, fi nd the substitution that is the most general unifi er (mgu) or explain why the two ...
• 211
744 views

### Ring Integration

In thinking about various methods of integration, I began to wonder if there was some sort of unifying theory relating integration and ring theory. For example, would there be a way to make sense of ...
• 4,768
657 views

### In unification, what cannot be unified?

Looking at various examples online, some seem concrete, but some seem to not be explained properly. Can $f(x)$ be substituted with $g(x)$? I know that $x$ cannot be substituted with $f(x)$, but $x$ ...
• 8,731
1 vote
345 views

### What is/How to do Unification

I'm reviewing for a final exam on Monday, and I have a question I was unable to answer on a previous test. The professor's notes were horrendous, and I can't find anything better online. They all seem ...
• 8,731
Let's let $\def\OP#1#2{\left\langle#1,#2\right\rangle}\OP xy$ represent the set $\{\{x\},\{x,y\}\}$ as is usual, per Kuratowski. Then:  \begin{eqnarray} \OP{\OP ab}c & = & \{\{\{\{a\}, \{a,...