Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [unification]

The tag has no usage guidance.

0
votes
1answer
37 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)...
0
votes
1answer
33 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 = ...
3
votes
0answers
50 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 ...
1
vote
1answer
33 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 ...
0
votes
0answers
64 views

Logic: general unifiers for expressions

How do i find the general unifier for each of the following pairs of expressions (there might be no unifiers for the expressions too) (a) foo(x,y) foo(y,x) (b) mother(x,y) mother(y,father(...
0
votes
0answers
107 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 ...
2
votes
1answer
69 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(...
1
vote
1answer
110 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))&...
1
vote
1answer
94 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 ...
0
votes
1answer
101 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
1answer
76 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 ...
2
votes
1answer
188 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 ...
1
vote
1answer
97 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
0answers
433 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 ...
2
votes
1answer
49 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?
0
votes
0answers
51 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
1answer
550 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 ...
1
vote
1answer
990 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))} - ...
2
votes
1answer
243 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 ...
4
votes
0answers
78 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 ...
2
votes
0answers
1k 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 ...
2
votes
1answer
3k 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 ...
2
votes
0answers
551 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 ...
2
votes
2answers
245 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$ ...
1
vote
1answer
252 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 ...
2
votes
1answer
303 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,...