Talk:Unification (computer science)

3616:

formalism. This entails preprocessing first their input and postprocessing their output when a substitution is produced. The overhead causes these linear algorithms to be slower on small sized arguments. Using a parser that generates an object-oriented C++/Java type representation can support (meta) annotations on formulas, terms, constants and variables. The linear DC algorithm uses 'object' variables with infrastructure for building substitutions. This makes this version also competitive on small sized input, [de Champeaux, D. Faster Linear Unification Algorithm. J Autom Reasoning 66, 845–860 (2022);

4133:[[ I want to add less than 10 pages to the wiki ... and notice how much trouble you create with your lack of ... of experience. You may be smart, but it does not work here. Trying to help me so that I can help improving the wiki? Doubt you can ... No relevant credentials anywhere. Please check my language because English is my 3rd one. ]] [[ BTW The talk page suggests to take out the Prolog stuff. Agree. Prolog never made sense when OO came on the scene (via Smalltalk). OO has added additional ways to decompose 'engineering' challenges. Reversing the order of <functionality & substrate: --> 2242:(non-ground) terms over 0,s,p,+,-,*; however, each such substitution could be instantiated to a ground substitution. Hence as a Corollary of Matiyasevich, unification w.r.t this E is undecidable. In this sense, this E can be viewed as the equational theory underlying Diophantine equations, with a grain of salt. You are of course right in that this E can't characterize ℤ up to isomorphism. Anyway, the argument of Dershowitz and Jouannaud about the distinction between word problem and unification problem would be worth to be explained in the article. 4166:

size arguments - by using richer formalisms. This requires preprocessing their inputs and postprocessing their output when a substitution is produced. Another approach relies on a 'fat' version of the predicate calculus using an OO architecture for formulas, terms, constants, variables (and axioms, definitions, lemmas, theorems, etc.) A parser can generate these expressions with optional support for (meta) annotations. An example is capturing in a hash table the variables in a formula (and term), which can be used to improve the occur check.

3887:[[ Let me add: the quicksort wiki is FATALLY wrong with its quadratic worst case complexity. A 1997 paper by David Musser gave a fix to get O(NlogN). The result? Java & Python use mergesort to avoid a quadratic blow up. Stupid. Slow and not in-place. Ditto with qsort on my ubuntu box. ChatGPT & Bard/Gemini regurgitate the O(N**2) complexity. The disasters get repeated ... and repeated ... and ... There are 2 people mentioned in the qs wiki 12&11 times. They made a cyberspace tombstone. Someone needs to clean them out. ]] 595: 585: 564: 1896:

theories themselves (which is of course well known for both). Next, there is a claim that unification is semidecidable for “Diophantine equations”. I don’t even know what that’s supposed to mean, as Diophantine equations as such are not a theory at all, but again, the given source (Matiyasevich’s paper proving the MRDP theorem) does not say anything about unification. There may be something I’m missing here, but as written, these examples do not make sense, and are unsourced.—

3025:, it is quite straightforward. Now that I look at it, it does not in fact prove confluence. The lead just refers to Martelli and Montanari's paper to say that a most general unifier (MGU) exists and the algorithm produces that unique answer. I guess if you wanted, you could expand the "proof of termination" to a "proof of termination and uniqueness" based on Martelli and Montanari's paper. It seems like a good idea, maybe you will be able to improve the article that way. 3593:

about using a 'rich' OO version of the predicate calculus: --- Formulas/ terms/ etc. have a hashtable attribute containing variables (used by the parser) -- which helps with the occur check --- Variables contain infrastructure for building substitutions and dealing with aliasing of variables exploiting the Union-Find algorithm Subclassing and/or adding attributes can enrich the semantics and 'pragmatics' of expressions.

4270:. Since higher-order unification is undecidable, there is in fact no algorithm for doing higher-order unification, so it can't be an algorithm, just like the halting problem is not an algorithm. Pedantically we could distinguish "a unification problem", "a unification algorithm", and "the process of executing a unification algorithm on a unification problem", but this doesn't reflect how people write about unification in practice. 2985:, and of course *I* can see it's more rewrite rules; 2) my/our objection remains: you try and implement those rules as written and you get an infinite loop: indeed YOU do try and prove that it's confluent and fail! (and note 8 is totally irrelevant, so what are you you even talking about??); 3) the focus of the article is not "logic", which is not even meaningful... I will fix that definition as soon as I find the time. 320: 677: 4105:

while the code might be longer, it will probably also be faster than the Java version. Your discussion of an "object-oriented" approach in the "faster" paper is really just a disguised method to use pointers instead of a hash table. In Java, the only way to use pointers is to make a class and instantiate an object of that class, but this is not the case in other languages.

243: 4686:(I would have cited it but there is nothing to verify for an example) It is non-trivial because it shows that unification is bidirectional. I guess I could have used "foo" like the source, I have no objection to changing it if you think it's clearer. I think though it is important to mention uninterpreted functions in the lead, the notion of syntactic equivalence doesn't make much sense without it. 222: 2002:

better to call it unification with constants for abelian groups. (I observe that unification with constants is not even mentioned in the article.) I still do not know what to make of the “Diophantine equations” example, but I begin to suspect that whatever the author may have intended also boils down to unification in the theory of commutative rings, as in the case of RCF.

191: 1687:, and that is what the opening paragraph says. Now, in systems which have bound and free variables, and one performs a substitution on a bound variable, then, yes, I guess you could think of it as being kind-of-like binding a value to a variable; but these are different ideas, really. Among other things, you can always make substitutions on free variables as well :-) 2566:"Postfix" refers to the order of the substitution "{x1 ↦ t1, ..., xk ↦ tk}" as a whole and its operand "t"; the former is written after the latter. See also the notation "tσ" in the same section. You are right if you meant that the operator "↦" is an infix operator; however, it is internal to the substitution and not referred to by the sentence you cited above. - 4219:

small sized inputs where the other linear versions are slower). Karen Oliver added to the wiki twice unacceptable sentences about my paper with references to me. My 3rd contribution - carefully crafted - is again ripped out by Mr Jochen Burghardt - totally ignoring my explanations here and without follow up on my clarifications. This is not acceptable.

3337: 728: 4488:, most papers treat it as a black box "we translated the problem to SMTLIB and fed it to Z3", but I think there is a significant amount of literature around the techniques used. I don't know if you are interested, creating new articles from scratch is a lot of work, but if you are, I would suggest creating a draft article in your user space, like 4440:

box. ChatGPT & Bard/Gemini regurgitate the O(N**2) complexity. The disasters get repeated ... and repeated ... and ... There are 2 people mentioned in the qs wiki 12&11 times. They made a cyberspace tombstone. Someone needs to clean them out. They are Sedgwick and Bentley. They block my papers already for a decade.

4475:

reader than your sentence "can be made equal through a substitution obtained by assigning values to variables in the two terms." But you are right that the article should explain the differences among forms of unification (first-order, higher-order, E-unification) in the lead, rather than just their application areas, so I have revised that part.

3192: 4783:

Knight, focussing on the simplest case of first-order logic before dealing with more exotic and less familiar logics. Here is a link to the paper: If this approach were taken, then Knight's characterisation of unification would cover the most common and familiar case and would be more faithful to the original notion of unification:

3651:"you removed a carefully crafted section - in vandalism fashion - in stealth mode/ without any notification -- twice i believe" This is the normal mode of editing on Knowledge, a section is added in one edit and then it is deleted in the next. This is the art of Knowledge - to not only make an edit, but to avoid having it reverted. 885:

m(x,x) and m(y,m(y,y)) where 'm' denotes multiplication. Can these terms be unified? I think so because they both begin with the same function symbol and have the same number of arguments, which - I believe - can themselves be unified. But the definition of unification given on this page does not cover binary (n-ary) functions.

1268:

and there it is misplaced: it belongs in the section on higher-order unification, as it's the canonical example of a higher-order unification algorithm, and because virtually every type-inferencing algorithm that I've come across for functional PL's use Robinson's first-order unification algorithm, not higher-order unification.

4299:, where we can present only the major improvements. Since your improvement (which I still don't fully understand from your article and discussion contributions; I'd like to read your paper, but didn't find an open-source version of it) didn't affect the computational complexity, I removed your addition; see my edit summary. - 4141:(A) The 'Further reading' section has an entry from Franz Baader and Wayne Snyder (2001). How about moving it to the reference section? I want to use it in my new section. And add it to the section 'Unification algorithms'. BTW: I found earlier a defect in the PW version (published) and recently a defect in the BS version. 3907:"two unpaid, unvetted, unaccountable volunteers." "A purpose of life is: help other people." "you not entitled to make that fuzzy assertion." "Spend way, way to much time tracking down the perpetrator" "This is NOT normal." "As an unvetted volunteer you can not assume a 'WE' authority stance. You are entitled only to ': --> 4693:

says "Couldn't match type ‘Bool’ with ‘’", which is a failure of unification, but an explanation of how unification is involved would probably take up the majority of the lead. An arity 2+ example is actually pretty rare in Haskell, as most type constructors only take one parameter. Most problems are

4218:

An earlier addition to this wiki was removed twice - vandalism style - by Jochen Burghardt without any notification on the talk page. Since then I have explained here page after page what is behind my linear unification paper (faster than all competition and also faster than the Robinson versions on

3969:

I don't think such an observation is correct. One can implement your Java algorithms in C or C++, and while the code might be longer, it will probably also be faster than the Java version. Your discussion of an "object-oriented" approach in the "faster" paper is really just a disguised method to use

3833:

this article.' Fatal ex-cathedra assertion." Well Knowledge does have pillars: in particular there is WP:NPOV and in particular WP:UNDUE. If there is only one article and it has 0 citations then it is hard to justify giving it more space in the article than a sentence, when there are so

3592:

believe< that it can be a 'game-changer' - google lingo - elsewhere in theorem proving; for example in the preprocessors for theorem provers that I wrote about 4 decades ago. Hence my section has the dual purpose of stating the progress of the algorithm AND that it dependent crucially

3092:

Related to this rule, the text says that it must decrease the number of variables that occur more than once, because it eliminates all other mentions of x. But what if t contains the only mention of another variable y? Wouldn't then this variable occur more than once afterwards, and show that this is

2716:

For instance the first substitution applied to g(x,z) produces t1 = g(f(u),z), while the second gives t2 = g(z,z). And t1 is not more special than t2. (Hence the two substitutions do not satisfy the standard definition of "more general": theta is more general than tau if tau is the composition

2083:

I didn't understand what you meant by "unification with constants" in general, since you seem not to consider unification in monoids as a special case of that. Anyway, the section on E-unification is admittedly still in a very preliminary state; you're welcome to explain unification with constants in

1895:

In the E-unification section, it is claimed that unification is decidable over Presburger arithmetic and the theory of real-closed fields. I’ve never heard of these theories in the context of unification, and the given references do not seem to support these claims, they are about decidability of the

1411:

Basically, three topics are mixed here: Theory-free unification, Theory-unification (also called equational unification) and Higher order Unification. All three topics are large enough for an own article -- what do you think is the best way to proceed without creating 2 stub articels which may not be

4782:

I hesitate to become involved in this unnecessarily unpleasant discussion. However, it seems that some of the problem may be due to the article's overly general approach, treating multiple kinds of logic simultaneously. A much better approach would have been to follow the lead of the survey by Kevin

4193:

Informatics has gone through the following sequence: Turing machines, hand coded hardware, assemblers, compilers for Fortran, machine instruction for multi tasking, recursion for Algol, C, Cobol, OO languages, C++, Java, concurrency & parallelism and these days ontologies. Each time other types

4120:

Being familiar with OO (check Google for my books) [and papers 9000+ reads], having written Mbs of Java code and having an OO version available for fol, I was able to exploit OO features to obtain a better/ competitive fol unification version. Could this be done also in assembly language? Sure, but

3143:

In citing the Paterson, Wegman paper, the article gives it a year of 1978, and therefore seems to give more credit to Martelli, Montanari (1976) But the year of 1978 is the date of the journal version of the Paterson, Wegman paper. There was an earlier publication from Paterson, Wegman in STOC '76

3028:

I myself am more interested in higher-order unification though, and there the MGU doesn't exist. It is for this reason that Huet's "algorithm" is only a semi-algorithm and all higher-order unification algorithms can get stuck in infinite loops evaluating possibilities for unification. So I would say

2966:

And I think the focus of the article is in fact logic. For one, the lead sentence says "in logic and computer science". I looked for a bit to find uses for unification besides in logic programming / proof search type applications but there really aren't any. The closest is "matching", which is where

2125:

Dershowitz.Jouannaud.1990 gives on p.284 a canonical term rewriting system (TRS) for addition, subtraction, and multiplication of integers, as an example for a theory where the word problem is decidable (by the TRS), but the unification problem is not (, since solvability of Diophantine equations is

1790:

As far as I understand unification (and I understand it fairly well), unification does not try to show that terms are equal (or identical), but rather determine if they have equal (or identical) instances. As an example, f(a,X) and f(Y,b) are neither equal nor identical, but have the common instance

1662:

Is Unification the operation that binds two terms, or is it the process that finds a solution to a whole theory? Some sections describe it as the former ("It represents the mechanism of binding the contents of variables and can be viewed as a kind of one-time assignment") and some as the latter (the

4259:

Well, I warned you... "given your previous writing style, it will probably get reverted if you add it unedited to the main page." And indeed, this was what happened. Jochen is pretty quick with the reverts, but even in the absence of Jochen and myself, most likely someone else would have eventually

4169:

The linear DC algorithm in uses 'object' variables with infrastructure for building substitutions, and for using the Union-Find algorithm to deal with variable aliasing and for the occur check +REF. This makes this version also competitive on small sized inputs. Using such a 'fat' version of the

4165:

Logic operations work typically with a LISP like representation for formulas, terms, constants and variables. The Robinson type algorithms exhibit exponential performance on them. The linear unification algorithms by Patterson-Wegman and by Baader-Snyder obtain their better performance - on larger

4111:

Sorry, things are getting worse. It is not even wrong. Suppose your parent needs a tool that reminds on their laptop to take medication X at time Y. Would you code that in assembly language? Fortran? C? C#? java-servlets? The choices are the 'same' from a theoretical perspective? The choices are

3993:

Please remove from the talk page your and this version of: <<< "two unpaid, unvetted, unaccountable volunteers." "A purpose of life is: help other people." "you not entitled to make that fuzzy assertion." "Spend way, way to much time tracking down the perpetrator" "This is NOT normal." "As

3837:

My paper is NOT about vanilla unification. It is about linear unification. I had one sentence about MY paper while I pointed out in the new section that richer languages have been used and are likely relevant also for other logic operations. {BTW I get still notification by ResearchGate about my

3792:

I did. Doubling down again. OK, show me ten papers about vanilla unification with correctness proof, code on GitHub & comparison/ performance tests against 3 competitors. OK, show me five papers about LINEAR unification with correctness proof, code on GitHub & comparison/ performance tests

3772:

This is NOT normal. Doubling down is even worse. I was totally confused by first seeing the addition and later it had disappeared. I checked the talk section: nothing. Spend way, way to much time tracking down the perpetrator: Jochen Burghardt. A consequence of not being trained, vetted, and not

3047:

Sorry again, for misreading a poor reply. Yes, the article is poorly written if at all correct(!), that was indeed the whole point! But it's true that any half-competent programmer understands what was actually meant, surely the first-order part, so I'll just fix that spec when I find the time...

2405:

Thanks for explaining the Diphantine equations theory, however I think that what I just said applies to it as well. It is a weaker theory than commutative rings, but it has undecidable unification for exactly the same reasons, so it does not illustrate anything new, and being an artificial example,

2109:

As for unification with constants, see section 3.2.2 of the Baader and Snyder chapter in the Handbook of Automated Reasoning for an explanation. The basic point is to consider unification problems involving additional free constant outside the signature of the equational theory. I might try writing

1267:

The description of higher-order unification is also just ... bizarre. What are ellipsis, in this context? IMO, it's easier to describe higher-order unification as "just" the process of unifying higher-order (lambda-) terms. Huet's algorithm is mentioned in the programming language section above,

1259:

The introduction seems hopelessly confused to me. For one, it doesn't even mention what constitutes a solution to a unification problem. As far as I'm aware, it's entirely standard to return a *substitution* as a solution to a unification problem, not another term, where applying the substitution

1131:

This is simply Prolog syntax: A = B is the unification operator, and it cannot be chained like A = B = C, one has to write it as several unifications joined by commas (which are really conjunction operators). I do not see any particular reason why a general article on unification should be bound by

1006:

Yes, BenKovitz and Kilgore666, you are right: The article is leaving out a number of important aspects and in my opinion it is complete rubbish in certain portions. It should be completely rewritten. In some parts the explanations really do hurt, since they are just not at all catching the meaning

884:

To say that x^2 can be unified with y^3 is at best misleading because the argument that (z^3)^2 = (z^2)^3 = z^6 is semantic and unification is - as I understand it - purely syntactic. I am not enough of an expert to get this right but it seems to me that as *terms* x^2 and y^3 have to be written as

851:

assume the reader wants to do it in Prolog/Lisp/etc. If there are any good web pages that explain unification on logic with a series of clauses containing nothing but plain ol' variables (not even quantifiers, just variables) as you would do logic problems on paper, I think a link to that would be

4588:

I guess you are right though about unification not being associated with Lisp, I have replaced it with a Prolog-based example. I am not sure though about going into detail with multiple different examples in the lead - that seems more suitable for a section. The "Formal definition" section already

3307:

Rereading our paper, I realized that independently both Robinson and (G. Huet and G. Kahn) came up with the simplified algorithm with and used the union-find algorithm to implement the equivalence algorithm. So if you are going to credit John Alan Robinson, you should also give credit to Huet and

3228:

It's a scanned PDF. I find it easier to read than the Martelli and Montanari reference but I'm hardly representative of most readers. You may find it easier too though. It's not important but the actual first version of that paper was an IBM RC in May '76, though that version had a minor error,

3062:

As for confluence, Martelli and Montanari have proved (on p.4 of their 1976 internal note) the algorithm to produce always a "solved form", which, moreover, corresponds to a most general unifier. It is straight-forward to show that two different most general unifiers need to variants of each other

1908:

Come to think of it, unification for real-closed fields is UNdecidable. To begin with, E-unification of terms only uses the equational part of the given theory, and the equational fragment of the theory real-closed fields is the theory of commutative rings. Anyway, since there is a constant in the

4474:

Regarding the lead, the article has to be at least somewhat accessible to non-technical readers. "Solving equations" is understandable to those with even a basic understanding of mathematics in a way that "investigating substitutions" is not. I think the example conveys more information to such a

4439:

Let me add: the quicksort wiki is FATALLY wrong with its quadratic worst case complexity. A 1997 paper by David Musser gave a fix to get O(NlogN). The result? Java & Python use mergesort to avoid a quadratic blow up. Stupid. Slow and not in-place. Ditto with qsort on my ubuntu

4104:

I had one sentence about MY paper while I pointed out in the new section that richer languages have been used and are likely relevant also for other logic operations. I don't think such an observation is correct. One can implement your Java algorithms in C or C++, and

3958:

I don't really see this distinction in the literature. All the algorithms for first-order unification are discussed equally. Whether they are linear or exponential is a matter of analysis, and if you analyze them empirically you will come to different conclusions on different datasets (and if you

3854:

wrote about 4 decades ago." - So then you write things? Are you in fact Dennis de Champeaux, as the d's and c's in your username might suggest? If so then it's a conflict-of-interest to cite your articles. Now per WP:SELFCITE it is allowed within reason (particularly note the

2496:

signs (because for some silly reason, the preprocessor wraps \stackrel’s in { } before passing them to LaTeX; \mathrel and friends are likewise broken). This is a long-standing problem, and I don’t know of a good way to work around this (inserting explicit \, fixes the texvc output, but makes the

1705:

to theory unification, i.e. unification modulo some (equational) theory. The first is decidable with a fairly simple algorithm. The second is not, in general, decidable, but semi-decidable. There are interesting instances that are decidable (unification modulo associativity and commutativity is a

781:

No; this is essentially the same concept as is used in various theorem provers and type checkers, and is not specific to Prolog or to computer programming. (Although in most "mathematical" uses of unification, the example A=f(A) fails rather than returning an infinite term; the extra step in the

4380:

The Unification operation investigates whether two pc terms are equal or can be made equal through a substitution obtained by assigning values to variables in the two terms. The operation terminates in fol with a unique 'best' substitution or with the conclusion that unification fails.

3615:

Logic operations work typically with a LISP like representation for formulas, terms, constants and variables. The Robinson type algorithms exhibit exponential performance on them. The linear unification algorithm by Patterson-Wegman (and others) obtain their better performance by using a richer

2401:

The article is too long as is, and I don’t think that artificial examples involving unsightly ad hoc lists of equations are helpful to the reader. The fact that an equational theory can have undecidable unification with constants even though elementary unification is decidable is certainly worth

1620:

In the termination proof, what is meant by "non-unique variable"? If the rules had names or numbers, the proof could list for each triple-component NUVN,NLHS,EQN the rules where it is decreased. (By the way: the proof is a good example for proving based on a well-ordering, but not by "structural

1263:

Also, nitpicking, but the section on first-order unification is mistitled. It isn't unification for first-order logic that is being described, but first-order unification, a description of the terms themselves to be unified (first-order terms, as opposed to higher-order terms or nominal terms).

4478:

Regarding your other suggestions, they seem great. I've incorporated your additional suggestions almost exactly as you suggested. It seems like you're really getting the hang of writing in Knowledge's style, which is fantastic to see. Regarding the "Logic Representation" section, I don't see it

2253:

as a term. When talking about term algebras, both notions coincide; else (e.g. in RCF, you said), they may differ. I think, this point should also be explained in the article - maybe even Dershowitz and Jouannaud (who certainly have a clue about this particular issue) jumped to conclusions when

2001:

I suppose unification over Presburger arithmetic is decidable by a similar argument, as it reduces to decidability of existential Presburger formulas. In any case, the equational fragment of Presburger arithmetic is the theory of abelian groups with an additional free constant 1, so it would be

800:

We really ought to distinguish between syntactic unification (discussed here) and E-unification (not yet discussed). E-unification is really important in automated theorem proving. Syntactic unification (and matching) also has important applications aside from Prolog; in ML-style languages, for

3148:

Note that in the Paterson, Wegman paper there is a description of an otherwise unpublished algorithm due to Robinson, which is significantly easier to describe than the one in this article. That algorithm is almost linear, but might be more appropriate for a Knowledge article because of it's

4116:

suggest< a LISP style (not code) for the data structures; this is detrimental - exponential complexity - for the Robinson-type versions. PW & BS used similar structures to get their linear versions - but still not competitive on small sized arguments due to input and output overheads.

3769:- in stealth mode/ without any notification -- twice i believe" - This is the normal mode of editing on Knowledge, a section is added in one edit and then it is deleted in the next. This is the art of Knowledge - to not only make an edit, but to avoid having it reverted. 3032:

3) There is a section "Application: unification in logic programming"... you clearly are in too much of a hurry. I would say to calm down and find some time to understand the subject, before attempting to make "fixes". Certainly the article is not very good, but at least it has some usable

2257:

After having had a glance at sect.3.2.2 in Baader and Snyder, I think, this distinction of elementary / with-constants- / general E-unification (which is somewhat new and isn't adressed at all by Dershowitz.Jouannaud.1990) should also be mentioned in the article; perhaps illustrated with

4420:

De Champeaux (2022) is also of linear complexity while also competitive with the Robinson algorithm on small size inputs. The speedup is obtained by using an object-oriented version of the predicate calculus. This avoids the need for pre- and post-processing. Variable-:

2854:

rule, we should express something like "recurs on G only", i.e., overall, we should rewrite the procedure to make the recursive call explicit, and what we are returning/how we are building the return value. (And, in any case, building it "in place" is per se not satisfactory: we want a

4747:

And doesn't it produce a solution set? It seems quite appropriate to describe the process as solving. Indeed, reviewing equation solving the description is identical other than that "equation solving" is generally over the real numbers and limited to one equation.

1260:

to input terms results in two alpha-equivalent terms. The notion of mgu is defined by taking an ordering on substitutions, not on terms. The polynomial example is completely unclear, as whether or not these two polynomials even have a unifier depends entirely on how they are encoded.

3877:

Bizarre ... You admit being useless/ obnoxious/ authoritarian/ ...? Remember your purpose? Helping other people. I try. You two don't. I invited you two to IMPROVE my new section - coming soon. Nothing but wasting our time. How about you do some solid research instead. Start with:

1761:

p.p.s. I've casually noticed that associativity seems to make a striking difference in decidability, (i've noticed it here and there), but I don't really get why, so both details, and general remarks on why associativity (and commutativity) seems to tilt things around, would be nice.

4411:

de Champeaux (2022) is of linear complexity in the input size but is also competitive with the Robinson algorithm on small size inputs. Champeaux attributes the speedup to using object-oriented programming techniques to avoid preprocessing and construction of a DAG.

4373:

design/solution<< realm, concocted by Montanari. (And is not linear at all.) [ This reminds me about programmers that start coding instead of:: ascertaining what the purpose is, subsequently make a design, and validate that against the reqs, and only then start coding, etc. ]

2070:

decidable. Hence, given any set of Diophantine equations, it is possible to enumerate all possible substitutions, checking for each one whether it is a solution. This would "semidecide" the equation set. Maybe, some of the preceeding should be said in the article, as an additional

4427:

Alternatively this paragraph is shortened while the new section is added wbout logic representation - see above. Just consider, for example, the problem dealing with time/situation as in McCarthy situation calculus by adding a param to a term. Instead the term can be enriched :

2005:

I thus propose to ditch the three entries, and possibly replace them with abelian groups with additional constants as an example of decidable unification, and commutative rings as an example of semidecidable unification. (As for references, these are both mentioned on page 486 of

4033:

Vukmirović, already in the article. And an older comparison of first-order algorithms here. I wouldn't say any of them are "complete" in the sense in comparing every published algorithm. Such a comparison would be useful but I guess is too tedious for anyone to have done. :

2105:

As for RCF, it is far from true that unifiability in decidable theories is decidable. The decision algorithm for RCF cannot provide witnessing terms, because (constant) terms in RCF only denote integers, whereas existential quantifiers need to be witnessed by arbitrary algebraic

4546:

The Unification operation investigates whether two pc terms are equal or can be made equal through a substitution. For example unification of: P(a) and P(a) succeeds P(a) and Q(a) fails P(a) and P(b) fails P(a) and P(x) succeeds with the substitution x-:

3450:

I didn't remove it; rather, I moved the essence of it (in particular the reference) up to the start of the section talking about complexity (cf. my edit summary). There are literally thousands of papers about unification, so we can't devote an own subsection to each of them. An

1541:

is quite nice. I tried to improve the rules' layout, using table alignment. The rules should possibly be named or numbered to ease referring to a particular one. Maybe a link to an article about presenting algorithms in rule form ("separation of logic and control", mentioned in

1305:

Hi, i wrote some semntences for HO unification, but its more a stub than something else. Explaining HO unification in detail requires lots of technical knowledge, so even an example is very hard to give. If you like, i can add some more stuff, but i don't know, if it is useful.

341: 2881:. The rules just represent the "logic" part; adding an arbitrary "control" strategy will lead to a correct unification algorithm (provided the strategy is "fair", i.e. every applicable rule is eventually applied). This is the reason why no explicit recursion strategy is shown. 3692:"for example in the preprocessors for theorem provers that I wrote about 4 decades ago." - So then you write things? Are you in fact Dennis de Champeaux, as the d's and c's in your username might suggest? If so then it's a conflict-of-interest to cite your articles. Now per 3738:

I have rewritten the new section with the better title 'Infrastructure for linear versions'. This deals with linear unification having different algorithms that rely on different data structures. It is NOT specific for my DC algorithm. It will be added to the wiki soon.

1682:

Don't know what you mean by "binding". In practice, unification is done on pairs of terms; in principle, you can take its reflexive, transitive closure which would make it apply to entire theories. I'll try to modify article to say this. ... Note: Unification is done with

1068:

Why speak of unifying "A=B, B=abc"? This is simply confusing. It is better to speak of unifying "A,B,abc" or "A=B=abc". There is no reason to mix equal signs and commas like that, when they mean the same thing in this context. I'm changing it to use commas throughout.

4073:

Homework: What is the time ratio on a 1024 array for insertionsort/ mergesort? Homework: What algorithm to use when the array is 512M and memory is 700M? Homework: Can the empirical results differ from the theoretical complexity analysis when the same language is used?

2079:

is decidable, too; if the theory decision algorithm happens to provide a witness term for each proven existentially-quantified formula, then an answer substitution can be constructed from it. I admit, that it may still be a problem to get a complete and minimal solution

3927:

2738:

I am not familiar with non-syntactical unification. I hope that the definition I introduced works also in such case. However I am unable to add a standard definition for a general case. It possibly should replace = by ≡ in σ = τη. But what is ≡ for substitutions?

4060:

Whether they are linear or exponential is a matter of analysis, and if you analyze them empirically you will come to different conclusions on different datasets (and if you analyze them theoretically you will reach a third set of conclusions).

4655:

Giving an example using Lisp function names does not imply that unification is just a Lisp issue. For these reasons, I'd still prefer the former version. If there are other, similarly popular, uninterpreted functions around (maybe nowadays in languages like

4483:

but perhaps a more focused article on representations used in implementations of logic provers could be written, perhaps with research on the representations AI models learn if more material is needed. I certainly have wondered about the implementation of

4022:

What makes you think that I am not willing to change an addition to the wiki if improvements/ critique is provided? Deletion of an addition is based on what authority? Who are you anyway? Are you helping other people? Have you published 500 page books?

1326:

I have started reworking the article, starting with the Introduction, removing all the technical jargon (we do not need to mention lattices in the introduction to a unification article). Any comments (in particular, any technical mistakes) are welcome.

3704: 4015:

I would say maybe to post it as a section on the talk page here (click "add topic" in the toolbar on the top), just because given your previous writing style it will probably get reverted if you add it unedited to the main page.

4260:

done the same, seeing as it is an unsourced section with quite different writing style from the rest of the page. That is just how Knowledge works - even the most finely crafted essay on quantum mechanics, if lacking sources, would get deleted as

3401:

Why was the new section 'Logic language representation' deleted? By whom? Why? It reports about a 2022 algorithm that improves the 1965 & 1978 versions AND introduces an OO version of predicate calculus --- allowing meta info to be added.

1791:

f(a,b) (with most general unifier {X<-b, Y<-a}). Similarly, if the background theory is {g(a)=b}, then g(X) and g(b) have equal instances (g(g(a)) and g(b), respectively), although the terms themselves are neither equal nor identical. --

4794:"The unification problem is most often stated in the following context: Given two terms of logic built up from function symbols, variables, and constants, is there a substitution of terms for variables that will make the two terms identical?" 4053:

Indeed the wiki is ordered along another dimension and ignores now the complexity (exponential vs linear) of the different fol versions. There is a treatment of the Robinson type fol version by Montanari. But not about the linear versions.

2406:

it would require listing all the equations above. (The undecidability of its unification problem also directly follows from undecidability of unification in commutative rings, since the two theories prove the same variable-free equations.)—

2074:

I don't have sufficient knowledge to follow your argument about undecidability of unification for real-closed fields (e.g. why are only integers admitted as ground unifiers). However, I think if the whole theory is decidable, then at least

3855:"only if it is relevant" clause), but also per WP:CITESPAM an academic author trying to persistently add a citation to their work without going through the proper processes is one of the most common reasons for banning people. 4203:

Certified low-level trivia garbage. Get out of the way. My linear unification algorithm relies on the availability of an object-oriented version of the predicate calculus (pc); and CANNOT be done effectively on a ... Turing-machine.

2999:

Sorry, I have just seen note 8: the thing is so poorly written and formatted that that portion goes off screen. It's a mess and very poorly written, it simply deserves a rewrite that is decently formal and not just that much handwaving.

1083:

Actually, I see why they are using equal signs. They are "unifying" a list of equations by separately unifying the terms that can be inferred to be equal in those equations. That is, whoever wrote those examples would say that unifying

4037:

Remember: the hyperbolic 'there are 1000 unification papers'? You don't show me ten papers about (fol) unification algorithms. You don't show me five papers about (fol) linear unification algorithms. Instead you refer to a paper about :

4046:

My paper is NOT about vanilla unification. It is about linear unification. I don't really see this distinction in the literature. All the algorithms for first-order unification are discussed equally.

3874:- You don't have to edit Knowledge... it is your choice to spend time here. Many people have left. There is a page Knowledge:Expert retention which discusses the fact that some (most?) experts get fed up pretty quickly. 153: 3933:

1743:' instead. These are really not the same thing, and some space should be devoted to this, as this is a point of confusion. More generally, I have yet to see any article on WP that really deals with syntax vs. semantics -- 1418:

The algorithm is very fuzzy explained -- what do you think of the algorithm of Martelli Montanari (this is the one with the rules of decomposition, variable elimination, occurs check and symbol clash, hope i did not forget

4029:

Show me ten papers about unification with correctness proof, code on GitHub & comparison/ performance tests against 3 competitors. There is the efficient higher-order unification paper by

4134:

and providing architectures with mini-ontologies, subconcepts, inheritance, encapsulation, etc. {Hoare logic breaks with the raw-wild-west semantics of pointer assignment. Encapsulation geofences the side-effects.} ]]

2723:

I am going to at least introduce a simple correction, replacing for "each variable x" by "for each term". (This is easier than introducing substitution composition.) Hope this does not introduce any new hidden error :)

3292:

You use the disjoint set union algorithm to maintain knowledge of equivalence. Actually way back when, I was taught the disjoint set union algorithm under the name "equivalence algorithm", so that's very natural.

4548:

a The operation terminates in fol with a unique 'best' substitution or with the conclusion that unification fails. Higher order logic unification can also fail or can produce one or more than one unifier.

1720:

I tried to carefully distinguish between "equal" and "identical" in the article: syntactic unification is about identity, not equality. If there are no equations, there cannot be any equalities, only identities.

4177:] 2nd Ref already available:: Baader, F. & W.Snyder, Unification theory, Chapter 8 in HANDBOOK OF AUTOMATED REASONING, Edited by Alan Robinson and Andrei Voronkov, Elsevier Science Publishers B.V., 2001. 2098:

The main problem with the “Diophantine equations” line is that saying that E-unification for Diophantine equations is semidecidable makes as much sense as saying that E-unification for apples is semidecidable.

1354:, which seems to want to cover unification in nominal equational logic. Before we get to the latest research topic (which you seem to be involved with), please write some more basic stuff missing. I wrote the 2592:

n. Given a type class instance Num Char, «1:» can be correctly inferred to have type . Therefore, I suggest to use another example here, like «1 : ('a', 'b')» which will fail to unify types and (b, c). --

3455:

certainly doesn't belong to this article. BTW: I doubt that Robinson's algorithm is faster than e.g. Martelli's and Montanari's, even for small terms, but nevertheless, I kept that claim of Champeaux. -

2237:

terms over 0,s,p,+,-,*, factorized by the congruence (say, E) induced by the TRS, is obviously isomorphic to ℤ. On the other hand, a unification oracle wrt. this E would return substitutions mapping to

1990:, and it has a ground unifier if and only if it has an integer solution. Thus unification over RCF (or for that matter, over any simple extension of the theory of commutative rings that does not prove 3753:

A purpose of life is: help other people. Knowledge is a great example but is vulnerable due to sociopaths. Its solution is using unpaid, unvetted volunteers, who create other problems. Here goes:

2040:

On the brighter side, many other theories have decidable unification problems, including Presburger arithmetic (Presburger , Shostak ), real closed fields (Tarski , Collins ) and monoids (Makanin ).

3603:(10) If you think that you can capture my content better how about you rewrite my section and put it somewhere. Otherwise please restore my section. Please notify me at: temp AT ontooo DOT com 3014:

1) Actually it was you, the first hit for "separation logic" is your comment of 14:56, 3 July 2023 (UTC). Jochen was discussing separation of logic and control, which is completely different from

2955:

formalism rather than a relational one - it's the same process of (nondeterministically) applying rules until no more rules are applicable. And of course one you prove the final result is unique (

3199:

I have included your STOC reference, and adapted the historical remarks. Since I don't have access to any of the Paterson,Wegmann papers, I can't check their description of Robinson's algorithm.

4000:" "Bizarre ... You admit being useless/ obnoxious/ authoritarian/ ...? Remember your purpose? Helping other people." "www.ontooo.com/AIAssessment2.pdf which I presented Feb 1 at ACDSA." : --> 365: 1909:

language, any unifiable set of equations has a ground unifier. Since every term is a polynomial with integer coefficients, any set of equations is equivalent to a set of polynomial equations

4200:

Factors such as programming language, programming style, input size, and whether the equations are unifiable or non-unifiable can affect the performance of a unification algorithm.

651: 2591:

This may sound a bit nit-picking, but the expression «1:» is not necessarily ill-typed. Number literals are overloaded in Haskell, so «1» isn't of type Int but actually of type Num n =: -->

4682:

I think the most common place people will encounter unification is Haskell or Prolog (I say Haskell but also include strict FP languages like Ocaml). The example is a Prolog example, from

4264:. I guess you find this unacceptable, like many experts who have attempted to edit Knowledge, but it is also one of Knowledge's core policies and I don't think it is changing anytime soon. 4070:

mergesort: time NlogN, space 2N insertionsort: time N**2, space N quicksort 1: worst time N**2, space N (average NlogN) quicksort 2: time NlogN, space N

1366:

article is still lacks major topics, including term rewriting and unification. You seem very into lambda-calculus stuff, but please (re)write this from a more general perspective. Thanks,

4689:

With Haskell, there is plenty of unification going on in H-M, but it is a bit complex to make the unification visible - it generally only shows up when something goes wrong. For example,

2064:

Of course, E-unifiability is semidecidable for recursively-enumerable E. ... 'British-museum' method of interleaving the production of substitutions with the search for equational proofs.

4194:

of applications became possible. Unix relied on functional code, GUIs relied on OO. As mentioned earlier: there is a feedback loop between applications and better languages/ metaphors.

4127:

I had one sentence about MY paper while I pointed out in the new section that richer languages have been used and are likely relevant also for other logic operations.

3913:" "Bizarre ... You admit being useless/ obnoxious/ authoritarian/ ...? Remember your purpose? Helping other people." "www.ontooo.com/AIAssessment2.pdf which I presented Feb 1 at ACDSA." 3349: 505: 2113:

No offence, but despite your expertise in other unification topics, none of the above persuades me that you have a clue about this particular issue, so I’ll go ahead with the changes.—

1849:", where unification of terms (rather than sentences) is explained, since I don't see anything particular to logical sentences here. Instead, the main contents is the explanation of " 147: 4358:

In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions, each of the form Left-hand side = Right-hand side.

3948:. I wouldn't say any of them are "complete" in the sense in comparing every published algorithm. Such a comparison would be useful but I guess is too tedious for anyone to have done. 44: 4422:

objects< become responsibility for creating a substitution and for dealing with aliasing. He claims that the ability to add functionality to predicate calculus : -->

2494: 1185: 3858:

Outrageous. Did you read my article? Did you see a self reference? I recommend, based on your persona - as shown, that you join law enforcement; you would likely thrive there.

1988: 977: 3970:

pointers instead of a hash table. In Java, the only way to use pointers is to make a class and instantiate an object of that class, but this is not the case in other languages.

1951: 422: 360: 1735:

And, as I read the above, I see that I misused the word "theory". Sigh.. my bad. However, this comes back to Diego Moya's initial point: for syntactic unification, we use '

4805:

The interpretation of unification as equation solving, which is the way unification is defined in this article, does not come up in Knight's 32-page survey until page 21.

2774:

The eliminate step in the algorithm seems wrong. I would suspect it to drop an element from the set in the right-hand side. This definition seems to loop. Anyone agrees?

2588:

and for the first argument "1" the polymorphic type variable "a" has to denote the type Int whereas "" is of type , but "a" cannot be both Char and Int at the same time.»

3809:- "we" is the community of Knowledge editors. You can see from this table that simply by having made more than 10 edits, you are in the top 5% of Knowledge users. 4953: 293: 283: 4537:

Again the 1st paragraph is TERRIBLE. Referring to solving equations is wrong; that is a metaphor used by Montanari to sketch a (lousy) design. Also using the notation:

3668:"'An OO version of predicate calculus certainly doesn't belong to this article.' Fatal ex-cathedra assertion." Well Knowledge does have pillars: in particular there is 3700:

an academic author trying to persistently add a citation to their work without going through the proper processes is one of the most common reasons for banning people.

3662: 4754:

Meanwhile, saying "pc terms" ("predicate calculus" terms as used in first-order logic?) is misleading as not all unification problems are first-order logic.

3964:

I had one sentence about MY paper while I pointed out in the new section that richer languages have been used and are likely relevant also for other logic operations.

2925:

to discuss at that level, but you say << ule "eliminate" is applicable only if the equation set contains "x=t" and some other occurrence of x outside of t : -->

2451:

Indeed, \textcolor and \leadsto are not supported by the default TeX rendering engine. They are supported by MathJax, which is probably why it went unnoticed so far.—

1596: 1572: 4570:

You say "referring to solving equations is wrong", but I'm not clear on how it is wrong. Doesn't unification start with a set of equations? And doesn't it produce a

4555:--- Take your ear-plugs out and listen to uncle Dennis who consulted for Fortune 500 companies to prevent them not doing their SW requirements homework thoroughly. 2433:

Failed to parse (unknown function '\textcolor'): \{ \textcolor{red}{y \stackrel{?}{=} nil}, \; a.v_3 \stackrel{?}{=} v_4, \; app(v_3,v_4) \stackrel{?}{=} a.nil \}

1861:". I also suggest not to define simultaneous unification of more than two terms formally, i.e., to simplify the explications about a set L of sentences/terms to. 4958: 1205: 2934:

specification, not a relational/equational one: all the more so in the context of a/any article whose focus is not per se logic programming or equational logic.

1872:" without agreement. An alternative could be to keep it, but to elaborate on the differences between unification of terms and sentences, making connections to 821:

I have added some more general statements to the article, and corrected some typos. These generalities should lend credence to keeping it as its own topic.

3789:

Hyperbolic, which weakens your stance" - This was actually not hyperbolic, see Google Scholar which says there are hundreds of thousands of papers,

259: 4968: 4948: 4207:

You get it now? Plus I argue that an enhanced pc that supports meta annotations most likely facilitates future logic reasoning and planning algorithms.

2951:

All the unification algorithms I've read are formulated similarly to the example algorithm, as a series of rules. I would argue the rules are based on a

2907:

If that doesn't convince you, try to make up a counter example, i.e. a unification problem and a sequence of rule applications that doesn't terminate. -

2062:

Concerning the source on Diophantine equations, I inferred the claim about semidecidability from the quote from Dershowitz.Jouannaud.1990, again p.282: "

641: 467: 79: 4405:... is slower than the Robinson version on small sized input due to the overhead of preprocessing the inputs and postprocessing of the output. 4973: 4479:

fitting in this article as this article is mainly about the concepts of unification rather than their implementation. There is an existing article on

1739:' to describe what's going on. But soon as one goes over to equational theories, or talks about satisfiability, and esp boolean sat, we use the word ' 1613:. If a potential eqn is generated several times, won't it be sufficient to solve it just once? That is, wouldn't the alg. work also with ordinary 3703:"I am 82 and dismayed that I need to spend time on you." - You don't have to edit Knowledge... it is your choice to spend time here. Many people 2948:

Regarding the eliminate rule, Jochen added a note 8 on eliminate which points out that x must appear in G, i.e. outside t. So yes, you missed it.

1415:

As mentioned by others below, first order syntax seems better to me than prolog syntax. Also the notion of unification problem should be present.

441: 2586:

The example in the article says «The Haskell expression 1: is not correctly typed, because the list construction function ":" is of type a-: -->

1290:

From reading the article I have *no* idea what higher-order unification is. DPMulligan has the right idea; this article definitely needs work!

4480: 3944:

There is the efficient higher-order unification paper by Vukmirović, already in the article. And an older comparison of first-order algorithms

2035:

Concerning the sources, here is a literal quote from Dershowitz.Jouannaud.1990 (see section "References"), p.282, sect. "Semantic unification":

1650:

e.g. Jörg H. Siekmann, Universal Unification, Proc. 7th Int. Conf. on Automated Deduction, Springer LNCS vol. 170, p.1-42, 1984 gives a catalog

617: 306: 250: 227: 3812:

Doubling down yet again. This is fatal. As an unvetted volunteer you can not assume a 'WE' authority stance. You are entitled only to ': -->

2967:

you are unifying a pattern with a closed term. That has some applications in higher-order term rewriting. But it's kind of a specialized use.

1490: 4963: 4769:

I am not sure though about going into detail with multiple different examples in the lead - that seems more suitable for a section.

3654:" 'There are literally thousands of papers about unification' Hyperbolic, which weakens your stance" - This was actually not hyperbolic, see 2258:

Burckert.1989's example of elementary unification being decidable, but unification with constants being undecidable (p.533-534 in his paper):

1034: 530: 85: 3680:

then it is hard to justify giving it more space in the article than a sentence, when there are so many highly-cited articles on unification.

2437: 168: 4006:<<< This is all very interesting but as it is out of scope of the article content I have replied on your talk page. : --> 3229:

which we corrected eventually (a test was placed in the wrong place in the algorithm, which effected correctness :-( but not performance).

1116:, actually performing two separate unifications. However, I think that this syntactic sugar is unnecessary for an introductory article. 135: 4627:

example, its solution is not obvious at first glance, so it gives an impression that unification might not be a trivial problem. As for

4144:(B) Please add my linear unification paper (#15 in the references) to the 'Unification algorithms' section after 'Baader-Snyder' of (A) 2548: 2522: 1014: 413: 4763:

I guess you are right though about unification not being associated with Lisp, I have replaced it with a Prolog-based example.

3939:

Show me ten papers about unification with correctness proof, code on GitHub & comparison/ performance tests against 3 competitors.

3371:

Request to replace the inline reference to an entry in the Reference section -- it is far beyond my abilities. Thanks. February 2024

3345: 3329: 2781: 1388: 1240: 1214: 828: 2850:

have to be considered "resolved"/have to be dropped from G, otherwise indeed all we get is infinite recursion: alternatively, in the

2796:

Your argument is tempting, but wrong. The algorithm is given in a form where the solution substitution is accumulated within the set

1507:

1.1.1. purely syntactically, i.e. wrt. an empty equational background theory - most existing stuff from the current article goes here

4834: 608: 569: 394: 4333:

The more recent addition is more manageable. I did expand it a little with some lines from the paper ("competitive", avoids DAGs).

2927:, which even makes sense, indeed closes the alleged "circle", but, unless I have missed it, the article does not say that anywhere. 2541:"Applying that substitution to a term t is written in postfix notation as t {x1 ↦ t1, ..., xk ↦ tk}". This is infix, not postfix. 3505:

Yes you removed a carefully crafted section - in vandalism fashion - in stealth mode/ without any notification -- twice i believe

4733:

No. That is just a metaphor. Unification is left-to-right traversal over the pair and decide failure or construct substitutions.

3164: 1518:

wrt. equational constraints) and particular equational background theories, which is currently only mentioned, but not explained

1351: 900: 4578:

the description is identical other than that "equation solving" is generally over the real numbers and limited to one equation.

2956: 1471: 486: 99: 30: 4187:[ My paper contains a reference to my GitHub unification repos, which has an implementation of a 'fat' predicate calculus. ] 1485:

1. Unification in general - Defn.: trying to solve a system of equations - Common notions (substitution etc.) - Applications:

129: 4296: 3112:

was already present before rule application (see the rule's left-hand side). So, if it contains the only occurrences of some

3022: 1603: 1599: 1575: 1551: 1547: 1538: 808:

I agree. This means that the dominance of Prolog should somehow be removed from the article. The right context to mention is

685: 104: 24: 20: 3390: 2930:

That said, on a more general note and FWIW, I'd contend that the most generic and readable expression of an algorithm is a

3677: 853: 74: 3029:

that first-order unification being terminating and confluent is a nice property but not really that important to discuss.

1835:

of two terms (or sentences) p and q, the notion "UNIFY(p,q)" made no sense; since it wasn't used elsewhere, I deleted it.

125: 3685:

believe< that it can be a 'game-changer'" - and do you have sources for this? Independent of the original article (

3341: 1511: 1370: 760: 451: 332: 202: 2084:

general and/or in particular theories, as well as unification in modal theories (I wasn't aware of the latter at all).

2018:

It might be also worthwhile to include some examples from modal logic, such as transitive modal algebras (decidable), K

4463: 4248: 3637: 3417: 3386: 2846:: namely, what you say may make sense but then a base case seems to be missing, to say that all equations of the form 2758: 461: 375: 65: 4197:

And what has been added to this wiki by an unvetted, overconfident volunteer (in response to what I want to add)??:

4170:

predicate calculus provides likely opportunities for other unification versions and for other deductive operations.

3063:

mod. renaming. So there can't be two essentially different outcomes of the algorithm, hence it must be confluent. -

1407:

Hi, i don't have much time to rewrite the article at the moment, but would ask you to give me feedback on my ideas:

175: 4930: 4673: 4304: 3708: 3461: 3212: 3180: 3128: 3068: 2912: 2833: 2571: 2563:(I moved the preceding remark from page top to here and added a section heading, in order to improve traceability.) 2392: 2089: 2050: 1998:) is equivalent to solvability of integer polynomial (i.e., Diophantine) equations, and as such it is undecidable. 1881: 1630: 1528: 812:; note that Prolog uses just a particular form of resolution. Higher-order unification should also be mentioned. -- 496: 258:

related articles on Knowledge. If you would like to participate, please visit the project page, where you can join

4810: 1355: 523: 4489: 4067:

Sorry, this does not make any sense. Doubt that you have a grip on computational complexity. Here an analogy:

1455:

I've done some work, introducing the idea of potential equatio, ans a nice mult-set based unifation algorithm.

4699: 4594: 4519: 4501: 4338: 4322: 4275: 3975: 3718: 3038: 2972: 2059:(In the preceeding quote, I replaced Dershowitz+Jouannaud reference numbers by the article's footnote numbers.) 1796: 1711: 1038: 2441: 2720:

In particular, {x/y} is not more general than {x/a} (Example 2.7, K.Apt "From logic programming to Prolog").

2552: 2526: 1018: 4493: 3433: 2245:

As for real closed fields, I see your point now: a formula "∃x: s=t" may be satisfied by a value for x that

1392: 1367: 1295: 1244: 1218: 832: 109: 3053: 3005: 2990: 2939: 2864: 1482:

I agree the topics should not be mixed in the current way. What do you think about the following structure?

1033:

What about the Most General Unifier? This article even redirects here, but the page does not mention it --

737: 4872: 4660:? Or in any other application area, not only in programming?), I have no objection to use them instead of 4446: 3313: 3298: 3160: 2960: 2785: 1740: 896: 809: 756: 141: 4313:

For accessing the paper, I found a Github link which is in the references. It is also available from the

1701:

Unification can refer to syntactic unification, i.e. finding a substitution that makes both terms equal,

1467: 4926: 4831: 4683: 4669: 4300: 3457: 3429: 3208: 3176: 3124: 3064: 2908: 2829: 2567: 2388: 2085: 2046: 1877: 1626: 1524: 870:

and referenced, I think. The Prolog page doesn't deal with it sufficiently on its own, and it matters.

432: 208: 2466: 1157: 871: 594: 4824: 4267:

Regarding "unification is an algorithm", there are various sources which define it as a process, e.g.

4173:

Refs::: [de Champeaux, D. Faster Linear Unification Algorithm. J. Autom Reasoning 66, 845–860 (2022);

2598: 1956: 949: 4806: 4451: 4236: 3918:

This is all very interesting but as it is out of scope of the article content I have replied on your

3625: 3405: 3374: 3352:

until a consensus is reached, and readers of this page are welcome to contribute to the discussion.

3152: 2777: 2746: 2544: 2518: 2463:

Fixed. Another problem with the default rendering is that spacing is wrong (viz. missing) around the

1736: 1672: 1622: 1459: 1384: 1332: 1276: 1236: 1210: 1142: 1010: 892: 888: 824: 789: 770: 764: 681: 4857: 4124:

There is a feedback loop between better languages and better applications. That is the reason for:

3749:

Please remove. I cover this in my new section. Also you not entitled to make that fuzzy assertion.

2900:. After it has been applied, the latter condition is false, so the rule is no longer applicable (on 1912: 190: 4876: 4695: 4590: 4515: 4497: 4334: 4318: 4271: 3971: 3714: 3686: 3034: 2968: 1792: 1707: 1428:

is the most prominent example, with prolog as a resolution based programming language as an example

1117: 1070: 992: 161: 55: 4639:

are what we call uninterpreted functions, without the need to be familiar with the latter notion.

3696:

it is allowed within reason (particularly note the "only if it is relevant" clause), but also per

1498: 1342:

Yeah, this article sucks. But before diving into it, perhaps its prerequisites should be written.

987:

true. What?? Is the example wrong or is the article leaving out a crucial piece of information? --

782:

unification algorithm which checks for this case and makes it fail is called the "occurs check".)

616:

on Knowledge. If you would like to participate, please visit the project page, where you can join

4914: 4889: 3994:

an unvetted volunteer you can not assume a 'WE' authority stance. You are entitled only to ': -->

3697: 3693: 3441: 3357: 3175:

Thanks for the STOC reference; I'll insert it when I have more time. For now, I just see the . -

2594: 1873: 1515: 1486: 1425: 1291: 1121: 1074: 1053: 600: 70: 4908: 4734: 4556: 4455: 4390:... (which I still don't fully understand from your article and discussion contributions; ... 4366:

Are two logic terms equal, can they be made equal through a substition or are they unequal?

4286: 4268: 4240: 4178: 3896: 3629: 3409: 3378: 2066:" I think, checking equality of ground instance of polynomial expressions over integers is even 584: 563: 4724:

You say "referring to solving equations is wrong", but I'm not clear on how it is wrong.

4582: 4485: 4040:

higher-order unification<<. These algorithms are totally different from fol algorithms.

3098: 2878: 1445: 1311: 351: 51: 801:

instance. Perhaps some discussion of the problem of coverage analysis would also be useful?--

4934: 4881: 4837: 4828: 4814: 4742: 4703: 4677: 4598: 4575: 4564: 4523: 4505: 4467: 4342: 4326: 4308: 4279: 4252: 3979: 3722: 3641: 3465: 3445: 3421: 3361: 3317: 3302: 3216: 3184: 3168: 3132: 3102: 3072: 3057: 3049: 3042: 3015: 3009: 3001: 2994: 2986: 2976: 2943: 2935: 2916: 2868: 2860: 2837: 2789: 2762: 2733: 2602: 2575: 2556: 2530: 2504: 2458: 2445: 2413: 2396: 2120: 2093: 2054: 2029: 2013: 1903: 1885: 1812: 1800: 1771: 1756: 1730: 1715: 1696: 1676: 1634: 1532: 1475: 1449: 1396: 1375: 1359: 1347: 1336: 1315: 1299: 1280: 1248: 1222: 1146: 1125: 1078: 1057: 1042: 1022: 996: 904: 874: 856: 836: 816: 793: 774: 403: 255: 4417:

programming technique<. It relies on a different (OO) representation of the pc. Hence::

4738: 4560: 4459: 4244: 3919: 3814:

I<< believe that XYZ'. Just consider the connection between authority and fascism:

3673: 3633: 3413: 3382: 3309: 3294: 3274:

An equivalence relation on the nodes of a dag is valid if it has the following properties:

3202: 3156: 2754: 2729: 2501: 2455: 2436:

I think this is related to LaTex. You can delete this section if I've made a mistake :)

2410: 2117: 2026: 2010: 1900: 1767: 1752: 1726: 1692: 1668: 1581: 1557: 1328: 1272: 1136: 3996:

I<< believe that XYZ'. Just consider the connection between authority and fascism:

3909:

I<< believe that XYZ'. Just consider the connection between authority and fascism:

3655: 3547:(cf. my edit summary). Yes you did because you did not appreciate the section added. 1381:

The article is good on syntactic unification but unclear on other forms of unification.

3665:

that simply by having made more than 10 edits, you are in the top 5% of Knowledge users.

3648:

Dear Ddccc, thank you for your contributions. I will go through and answer your points:

1841:

The notion of applying a substitution to a set of sentences still remains to be defined.

4511: 4433:[[ BTW The PW version is NOT using the Union-Find algorithm -- quite remarkable ... ]] 3669: 2254:

claiming a decidable unification problem (rather than only a decidable theory) for RCF?

1808: 1664: 1494: 1463: 1343: 988: 477: 319: 3289:(iii) the equivalence classesmay be partially ordered by the partial order on the dag. 1190: 342:

Requested articles/Applied arts and sciences/Computer science, computing, and Internet

4942: 4381:

Higher order logic unification can also fail or can produce more than one unifier.

3437: 3353: 3350:

Knowledge:Redirects for discussion/Log/2022 September 19#Narrowing (computer science)

3283:(ii) each equivalence class is homogeneous,that is it does not contain two nodes with 2959:), then the rewriting system defines a function. Rewriting is a natural extension of 1049: 802: 4892: 3253:

r$ '$ $ \equiv$ s$ '$ unknown for a pair of corresponding sons r $ '$ , s$ '$ ):

4574:? It seems quite appropriate to describe the process as solving. Indeed, reviewing 4571: 4261: 3232:

Here's a latex version of Robinson's faster algorithm. It's time is $ n\alpha(n)$

3094: 2249:

as a term, while a solution of the unification problem "s=t" can only be something

1684: 1441: 1307: 3277:(i) if two function nodes are equivalent then their corresponding sons are equiva- 2384:, ..." amounts to DA-unification, "... and hence unification will be undecidable." 1827:

I made some changes in section "Definition of unification for first-order logic":

1048:

I have now tried to add the definition of MGU to the article. Hope this is helps.

724:

Discuss higher-order unification and various kinds of non-first-order unification.

4115:

The fol algorithms in the wiki were developed pre OO and their descriptions : -->

3498:(1) Thx for adding my paper the reference section. (2) I didn't remove it; 2402:

pointing out, but I’d leave out the counterexample, a reference should be enough.

4363:

purpose< is of unification; for example a special case of pattern matching:

3591:

representation< of the logic language makes a key difference - and I : -->

2742:

So a competent look of someone familiar with general unification is necessary.

2368:"In this theory every unification problem is trivially solvable by substituting 813: 783: 613: 3225: 3145: 1546:) should be added. Some notation needs to be unified: "no solution" in section 4514:, each talk page is intended for discussion only of its accompanying article. 4112:

the same from a pragmatic perspect? Why do you select a particular language?

3661:"Who is 'we'?" - "we" is the community of Knowledge editors. You can see from 2750: 2725: 2498: 2452: 2407: 2114: 2023: 2007: 1897: 1763: 1748: 1722: 1688: 1133: 590: 4619:, we need an uninterpreted function of arity ≥2. Due to the 2 occurrences of 4174: 3711:

which discusses the fact that some (most?) experts get fed up pretty quickly.

3684:

representation< of the logic language makes a key difference - and I : -->

3617: 3144:

from May of 1976 paper that was almost the same as the journal version. See

4543:

is crazy. We are not doing LISP here. Here a 2nd alternative: <<<

2952: 2430:

It might be my browser, but I seem to get a lot of error messages? Example:

1744: 1543: 1363: 384: 4362:

This is all seriously WRONG. The 1st sentence should convey what the : -->

3953:

My paper is NOT about vanilla unification. It is about linear unification.

3746:

According to Champeaux, Robinson's algorithm is faster on small inputs.

242: 221: 4098:

The timings of the linear versions are proportional to the Size argument.

3945: 3838:

papers from 40, 30, 20 years ago and from recent papers about quicksort.}

3589:

to this article. Fatal ex-cathedra assertion. Unification is : -->

3259:

Test the relation `$ \equiv$ ' for conditions (ii) and (iii) of validity.

4225:

In logic and computer science, unification is an algorithmic process ...

4885: 4314: 3336: 2828:). I'll add a corresponding note to the article; thanks for the hint. - 2816:

rule isn't applicable more than once, since after its first application

1362:

one a while back, but don't have much time to contribute lately, so the

4917:

in your discussion style, and avoid personal attacks and phrases like "

4657: 4585:?) is misleading as not all unification problems are first-order logic. 3554:(6) There are literally thousands of papers about unification, so 4228:

is already wrong. It is not a process. Unification is an algorithm.

3959:

analyze them theoretically you will reach a third set of conclusions).

3590:

functional< code. It turns out that an OO approach to the : -->

3582:(8) An OO version of predicate calculus certainly doesn't belong 4684:

https://www.dai.ed.ac.uk/groups/ssp/bookpages/quickprolog/node12.html

1132:

syntactic conventions of a specific language, your change is fine. —

867: 4581:

Meanwhile, saying "pc terms" ("predicate calculus" terms as used in

4424:

objects<< provides opportunities for other logic operations.

3793:

against 3 competitors. FOLLOW UP instead of shouting in the void.

3540:(5) up to the start of the section talking about complexity 2884:

Rule "eliminate" is applicable only if the equation set contains "

2110:

something about it later, but I don’t have the time at the moment.

3825:"'An OO version of predicate calculus certainly doesn't belong to 4615:

be understandable without much explanation. In order to achieve

3610:

Here is my section: <<< Logic language representation

3568:(7) we can't devote an own subsection to each of them. 1838:

The notion of a unifier of a set of sentences had to be defined.

4399:... is slower than the Robinson version on small sized inputs. 3761:"you removed a carefully crafted section - in vandalism fashion 3340:

An editor has identified a potential problem with the redirect

2045:

Concerning your arguments, I'll try later to understand them.

667: 460:

Find pictures for the biographies of computer scientists (see

184: 15: 4717: