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 ...
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 ...
137 views

How can I compute the most general unifier for these two expressions?

I have the following first order logic expressions: $f(g(a, h(b)), g(x, y)),~f(g(z,y), g(y, y))$ and I want to compute the most general unifier for them. If I follow the algorithm found on these ...
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 ...
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 ...
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 ...
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 ...
1 vote
28 views

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 ...
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 ...
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 ...