Questions tagged [unification]
The unification tag has no usage guidance.
2
votes
1answer
33 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 ...
1
vote
0answers
13 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 ...
1
vote
0answers
38 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 ...
2
votes
1answer
90 views
Why this pattern matching fails in Agda?
Consider function wa'' (need natural number definition, either in stdlib or Agda.Builtin.Nat):
...
4
votes
1answer
57 views
E-Unification: “Goal seeking” pattern matching between directed trees
Preamble
Suppose we have some symbols x, y, ... and wildcards (ξ), ...
2
votes
0answers
121 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 "...
2
votes
0answers
86 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,...
2
votes
1answer
48 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 ...
2
votes
1answer
100 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 ...
1
vote
1answer
50 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 ...
2
votes
0answers
15 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 ...
1
vote
1answer
125 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 ...
8
votes
1answer
148 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 ...
0
votes
0answers
140 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 ...
0
votes
1answer
43 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 ...
4
votes
1answer
1k 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 ...
6
votes
1answer
195 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 ...
6
votes
1answer
795 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:...
7
votes
2answers
331 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....
1
vote
1answer
68 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) ...
2
votes
1answer
33 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:
...
3
votes
1answer
366 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?
3
votes
2answers
729 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 ...
1
vote
1answer
111 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 ...
6
votes
3answers
6k 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 ...
4
votes
2answers
298 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 ...
3
votes
1answer
154 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 ...
10
votes
1answer
570 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 ...
15
votes
3answers
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.
...
