# Questions tagged [unification]

The tag has no usage guidance.

41 questions
Filter by
Sorted by
Tagged with
1 vote
26 views

### Datastructures for finding unifiable terms

I am looking for a datastructure that supports the following operations: Add a term Remove a term Return a pair of unifiable terms if one exists. Ideally, 3 would be as close as possible to ...
• 111
30 views

### How can I prove KB╞ α?

Is correct to use ~α as rule to prove KB╞ α? Is possible to unify sentence ~V(x,y) v S(x) with V(N,W)? ...
43 views

### Unification with a list of terms

The problem: we have a list of terms $[t_1, ..., t_n]$ , and a term $t$, and we want to find which of the terms in the list can be unified with $t$. Obviously we can iterate through the list and check ...
• 23
36 views

### Is type unification a kind of search for alpha equivalence?

I was reading about type unification and it moves through of substitution of variables. To me it looks like a search for an alpha equivalence... I mean, two types are unifiable if they are alpha ...
• 243
1 vote
30 views

### Unifiers modulo commutativity in terms of syntactic unifiers and $\approx_{C}$-class

I am studying Term Rewriting by reading Baader's book "Term Rewriting and All That". I am in the chapter of Equational Unification, in the section of Commutative Functions. I am trying to do ...
94 views

### Unification Algorithm without Occur Check

I have been reading about Unification algorithm here https://en.wikipedia.org/wiki/Unification_(computer_science)#A_unification_algorithm . And I wonder about the importance of occur check. I know ...
• 33
101 views

### Inference and Unification algorithm provided to a Unification graph of two expressions

I am trying to unify two expressions given a unification algorithm $unify$ applied to the unification graph of the two expressions. However, I struggle a lot in understanding how exactly the steps of ...
• 143
1 vote
29 views

### Injectivity not required for unification algorithms?

When learning about a general unification algorithm, we learned the rule decompose, which states unifying $$G \cup \{f(a_0,...a_k)=f(b_0,...,b_k)\} \Rightarrow G \cup \{a_0=b_0,...a_k=b_k\}.$$ The ...
• 469
1 vote
28 views

• 1,654
7k views

### Can someone clarify this unification algorithm?

I've been having trouble understanding a unification algorithm for first order logic, as I don't know what a compound expression is. I googled it, but found nothing relevant. I also don't know what a ...
• 726
346 views

### Unification --- most specific unifier

In unification, given a set of equations, a standard problem is to compute a most general unifier (mgu). I am interested in a somewhat reversed problem. Imagine having a set of equations that do not ...
• 1,654
216 views

### Type inference of pair (product) types

I am looking into Hindler-Milney type system and I am trying to add support for the pair type. In Pierces book, he introduces special language constructs for creation of pairs and getting their ...
• 1,654
878 views

### Unification vs. SAT solver

I read on Wikipedia that unification is a process of solving the satisfability problem. At the same time, I know that such solvers are called "SAT solvers" or "SMT solvers". So, are they different ...
• 1