Questions tagged [unification]
The unification tag has no usage guidance.
37
questions
0
votes
0
answers
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 ...
- 1
0
votes
0
answers
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
0
answers
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
2
votes
0
answers
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
2
votes
0
answers
122
views
How does kommutation affect unification in first oder predicate logic
This was asked on an exam last semester. I know that my algorithm fails in this case, or does it not? because of the function being not the same like $g(f(x))=f(g(x))$.
The problem: given by 2 lists $...
2
votes
0
answers
42
views
Sufficient Criterion for Word Equivalence in Idempotent Semigroups
I am reading Baader's paper "The Theory of Idempotent Semigroups is of Unification Type Zero" and I have a doubt about a property of idempotent semigroups.
Let $AI = \{(xy)z = x(yz), x^2 = x ...
- 373
2
votes
2
answers
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)}
...
- 75
1
vote
0
answers
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
1
answer
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
0
votes
1
answer
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. ...
0
votes
1
answer
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
-1
votes
1
answer
77
views
Most General Unification in Prolog-EBG algorithm
I am reading the algorithm of prolog-EBG in Machine Learning by Tom Mitchell, and the following algorithm has a step to compute a most general unification:
$\theta_{hl}:$ the most general unifier of $...
- 143
0
votes
1
answer
287
views
most general unifier: can a variable be substituted to a variable and a function?
i was wondering: when doing most general unifiers(MGU), can a variable be substituted to a variable and to a function?
examples that illustrates my question:
1)loves(girlfriend(x),x) , loves(y,y)
2)...
- 23
0
votes
1
answer
71
views
finding the most general unifier
i am trying to find the most general unifier of the following:
1)Daughter(Uncle(y),y), Daughter(Uncle(x),emily)
2)Loves(cat(x),x), Loves(y,y)
what i think:
1)$\theta = [emily/y, x/y]$
2)$\theta = ...
- 1
3
votes
0
answers
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
1
answer
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 ...
- 87
0
votes
0
answers
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 ...
- 460
2
votes
1
answer
278
views
Checking Most General Unifier
I've just taken a logic course in college. However, there's something that I'm still unsure about MGU. I will like to use an example to illustrate my query.
Suppose we have to unify $Q(y, G(A,z)), Q(...
- 151
1
vote
1
answer
320
views
How to unify a pair of atomic formulas?
Unify the pair of atomic formulas $p(a,x,f(g(y))),\ p(z,h(z,u),f(u))$.
Attempt following the alogrithm described below.
We have
\begin{align}
\begin{aligned}
a &=z\\ x &=h(z,u)\\ f(g(y))&...
- 460
1
vote
1
answer
186
views
First Order Logic Resolution
During Resolution, Can a skolemization constant be replaced by a function?
For example:
∃X e(X)∧ g(X)
After replacing with skolemization constant
...
- 57
0
votes
1
answer
161
views
First Order Logic, help in Unification and substitution process
I'm trying to solve a few unification problems, but this one is a bit tricky to me. I have to demonstrate how to derive the first one starting from the second one.
$\phi$ (c, f(c,h(M,e(c)))
$\phi$ (...
0
votes
1
answer
120
views
Can this given set be unified?
Assuming a,b,c are constant, and the rest are variables, what is the result of unification to the following sets?
P(f(x,z),r,t) , P(w,f(g(w),h(t),b)
The obvious solution would be to do the ...
- 5
2
votes
1
answer
905
views
Using the unification algorithm to determine whether pairs of formulas are unifiable
I would like to use the unification algorithm to determine whether or not the following pairs of formulas are unifiable, and if so, find a most general unifier, showing all my working. Am I doing it ...
- 285
1
vote
1
answer
259
views
Most General Unification of variables with the same function
I have to find the Most General Unifier of the following atomic sentences
P(x1,G(x2,x3),x2,B) and P(G(H(A,x5),x2),x1,H(A,x4),x4)
After using the Martelli-Montanari Algorithm I ended up on the ...
0
votes
0
answers
545
views
Unusual most general unifier example
we're trying to unify the following:
P(x,f(y)) and P(z,z)
(where P is a binary predicate, f is a unary function and x,y,z are variables)
Following the algorithm, I first include the following ...
- 249
2
votes
1
answer
215
views
Unification of $P(x,x)$ and $P(a,b)$ [closed]
Why can we not unify $P(x,x)$ and $P(a,b)$? Don't the substitutions $a/x$ and $b/x$ provide unification?
- 87
0
votes
0
answers
54
views
Is this unifiable? SDLNF Derivation of the Generic Goal.
I found a problem which is a definite program problem and ask to obtain all SDLNF derivations of the generic goal.
$Product(x,y) ← Quantity(x),Rate(y)$
$Rate(x) ← Sub(x)$
$Quantity(a)$
$Quantity(b)...
1
vote
1
answer
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
2
votes
1
answer
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
3
votes
1
answer
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 ...
- 43
5
votes
0
answers
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
3
votes
0
answers
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
3
votes
2
answers
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
2
votes
0
answers
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
2
votes
2
answers
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
1
answer
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
2
votes
1
answer
422
views
Unification of expressions involving sets
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,...
- 63.5k