Questions tagged [unification]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0 votes
0 answers
13 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)? ...
user avatar
0 votes
0 answers
12 views

An efficient algorithm for determining unifiable pairs

The first order resolution rule is given as: $$\frac{P\lor L_1 \qquad \neg Q \lor L_2}{L_1 \sigma \lor L_2\sigma}$$ where $\sigma$ is the most general unifier of $P$ and $Q$. Therefore, one is asked ...
user avatar
  • 171
2 votes
1 answer
28 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 ...
user avatar
  • 23
0 votes
0 answers
30 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 ...
user avatar
  • 219
1 vote
1 answer
24 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 ...
user avatar
2 votes
1 answer
63 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 ...
user avatar
  • 23
0 votes
1 answer
63 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 ...
user avatar
  • 123
1 vote
1 answer
26 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 ...
user avatar
  • 409
1 vote
1 answer
25 views

Why does the substitution {x/f(y), y/z} work this way?

There is an example of applying a substitution to an expression, and I am having a problem with it. Let $\theta = \{ x/f(y), y/z \}$, and $E=p(x,y,g(z))$, then $E\theta = p( f(y),z,g(z) )$. Why is $...
user avatar
  • 21
2 votes
1 answer
56 views

What algorithms for unification over (multidimensional) array terms?

I am looking for references on implementing unification over multidimensional array terms. Are there specialized unification algorithms for those cases? I wasn't able to find satisfactory literature ...
user avatar
  • 205
1 vote
0 answers
55 views

Can the most general unifier be defined categorically?

I remember from my reading of Category Theory for Computing Science that classical concepts like weakest preconditions can be seen as the categorical notion of pullback. I was wondering if the same ...
user avatar
  • 2,220
4 votes
1 answer
76 views

Is unification over regular expression equations doable?

By way of example, suppose I know that $X + a = b + Y$ where $X$ and $Y$ are variables standing for regular expressions, then $(X, Y) = (b, a)$ is a solution to this set of equations. Generalizing ...
user avatar
2 votes
1 answer
93 views

Is Unification "an Implementation of Existential Quantification"?

I read a comment (I've forgotten the source), "Unification is an implementation of existential quantification." (Emphasis mine.) If true, this point of view clears up many things. For instance why ...
user avatar
  • 143
1 vote
0 answers
86 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 ...
user avatar
2 votes
0 answers
58 views

Unification algorithm that directly finds multiple substitutions?

Systems of formal logic generally have inference rules that require certain expressions to be syntactically the same in multiple steps. Typically two steps are involved, as for modus ponens, where ...
user avatar
  • 121
2 votes
1 answer
300 views

Why this pattern matching fails in Agda?

Consider function wa'' (need natural number definition, either in stdlib or Agda.Builtin.Nat): ...
user avatar
  • 888
4 votes
1 answer
78 views

E-Unification: “Goal seeking” pattern matching between directed trees

Preamble Suppose we have some symbols x, y, ... and wildcards (ξ), ...
user avatar
  • 141
2 votes
0 answers
193 views

Most efficient unification algorithm?

I've been trying to find the most efficient unification algorithm by following reference chains on the Wikipedia article on unification. As far as I can tell, the fastest one is the one presented in "...
user avatar
2 votes
0 answers
112 views

Unification algorithm - need clarification

I have these two terms: {P(a,x,x),P(a,b,c)} I'm supposed to find if the terms and unifiable using the unification algorithm. I'd do the following substitutions: b/x, resulting in : {P(a,b,b),P(a,b,...
user avatar
2 votes
1 answer
58 views

"not provable", what does this to do with unification?

I found one interesting point in nominal unification. Just after proposition 2.16 of Nominal Unification by Urban, Pitts, and Gabbay, it said the following, which I found confusing: For non-ground ...
user avatar
  • 1,042
2 votes
1 answer
145 views

Are these examples of unification problems?

I have been studying unification, especially nominal unification (paper) gets my attention. I read the theory and examples. But I am wondering that what kind of problems occur in unifications. For ...
user avatar
  • 1,042
1 vote
1 answer
52 views

is this an example of nominal unification?

I am thinking that is the following a problem solved by nominal unification. $\lambda a.X = \lambda b.\lambda c.c $ where we find $X$. The answer is obvious. The reason is that it seems in nominal ...
user avatar
  • 1,042
2 votes
0 answers
21 views

Need clarification in theorem about syntactic equations and substitutions

In the book "Constraint Handling Rules", Thom Frühwirth explains (on p. 50) "Substitutions, variants and equality" over a usual first-order logic language composed of variables, function symbols and ...
user avatar
1 vote
1 answer
214 views

Comparison Procedure in Robinson's Unification Algorithm

I'm studying the Principal Type (PT) Algorithm in Basic Simple Type Theory by J. Roger Hindley. One step to find the PT of a term is the Unification of types. The Robinson's Unification Algorithm uses ...
user avatar
9 votes
1 answer
188 views

Is there a general algorithm to fill holes in terms of the Calculus of Constructions?

Suppose that you extend the Calculus of Constructions with "holes" - i.e., incomplete pieces of code that you didn't fill yet. I wonder if there is an algorithm to fill those roles automatically. For ...
user avatar
  • 4,017
0 votes
0 answers
239 views

what is a disagreement set in nominal unification?

In unification, for example set $s=\{ f(a,Y),f(X,d) \}$ has a disagreement set $\{ (a,X),(Y,d) \}$, since these two elements does not match on their fields. simply speaking that is a set disagreement ...
user avatar
  • 1,042
0 votes
1 answer
55 views

occur-check, does nominal unification has it?

In unification, there is a "occur-check". Such as $X = a \, X$ fails to find a substitution for $X$ since it appears on right hand side too. The first-order unification, higher-order unification all ...
user avatar
  • 1,042
4 votes
1 answer
2k views

How can unifying 2 sentences in first-order logic result in a variable becoming 2 different things?

I'm working on a program which must use inference in first-order logic, and everything is working great except for 1 thing which I don't understand. The book I'm using, "Artificial Intelligence A ...
user avatar
  • 143
6 votes
1 answer
251 views

why nominal unification is a first-order unification?

In my understanding, if a unification solves equations of terms that are not higher-order terms, then it is a first-order unification. If a unification solves equations of terms that are higher-order ...
user avatar
  • 1,042
6 votes
1 answer
1k views

What is a unifier?

Currently I read up on unifiers, however have some problem understanding its concept. Thus far I found an example of an equation: add(suc(x); y) $\stackrel{.}{=}$ add(y; suc(z)) and unifiers to it:...
user avatar
  • 415
7 votes
2 answers
432 views

Generating constraints to solve dependently-typed metavariables?

In dependent-types, Miller pattern unification is used to solve a decidable fragment of higher-order unification. This allows dependently-typed languages to contain metavariables or implicit arguments....
user avatar
  • 29.1k
1 vote
1 answer
95 views

Unification Functions

I need to apply the unification function to unify the following expression: foo(X,X,Y) and foo(Z,p(Z),w) So far, I've determined that I must substitute 'w's for occurances of 'Y', making foo(X,X,w) ...
user avatar
2 votes
1 answer
42 views

Can high-order unification be applied to programming by example?

In 2007, it has been proven that high-order unification is decidable on the pattern matching case. If that is true, what is stopping someone to write an equation like: ...
user avatar
  • 4,017
5 votes
1 answer
612 views

Term Rewriting vs Unification

How is term rewriting different from unification, and what's the difference between term rewriting languages and logic programming, like Prolog?
user avatar
  • 445
4 votes
2 answers
1k views

Skolemization with multiple arguments -- how to unify

Edit: answerers keep finding (valid!) problems with my example. I'll try again. The older version is below the horizontal line. Thanks to Klaus below for pointing out the last problem. My ...
user avatar
1 vote
1 answer
119 views

Unification --- removing equations and updating the solution

This question is concerned with the first order unification. Suppose I have a set $D$ of equations and a solution to these equations. Let this solution be a set $S$ of substitutions. Now, suppose I ...
user avatar
  • 1,604
6 votes
3 answers
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 ...
user avatar
  • 686
4 votes
2 answers
331 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 ...
user avatar
  • 1,604
3 votes
1 answer
200 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 ...
user avatar
  • 1,604
13 votes
1 answer
786 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 ...
user avatar
  • 1
17 votes
3 answers
3k views

Why is unification so important to inference engines?

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. I keep reading about the Unification Algorithm. ...
user avatar
  • 5,002