Questions tagged [unification]

The tag has no usage guidance.

7 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
2
votes
0answers
47 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
0answers
155 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
100 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
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
0answers
25 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 ...
0
votes
0answers
32 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 ...
0
votes
0answers
163 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 ...