5 ms·

On a related note, I recently learned about the relationship between theorem provers and unification [1][2]. I was actually just trying to understand "plain" u

On a related note, I recently learned about the relationship between theorem provers and unification [1][2]. I was actually just trying to understand "plain" unification (still working through it!). I just find it exciting to discover cool applications of unif. that I haven't came across before. (Btw, I'm trying to figure out how unification can be used as a building block for a datalog like query language for indexedDB) 1: https://eli.thegreenplace.net/2018/unification/ https://eli.thegreenplace.net/2018/unification/ 2: https://en.wikipedia.org/wiki/Resolution_(logic) https://en.wikipedia.org/wiki/Resolution_(logic)

YeGoblynQueenne 5y ago
To understand unification I recommend Robinson's seminal paper on resolution, "A machine-oriented logic based on the resolution principle", which is also referenced in your first link. It's a widely influential paper and most modern work on unification, theorem proving, logic programming etc derives from it to some extent. It's an old paper and it might look scary on first sight but it's actually pretty readable. As an aside, I'm told that Robinson's paper was in review for well over a year in a constant back-and-forth between him and referees who kept demanding improvements. Which of course was very frustrating for Robinson, but it seems to have done the job and resulted in a very readable, very clear paper. Give it a try! Btw, I'm a bit put off by the terminology chosen in your first link that treats predicates as functions. Robinson of course describes unification in first-order logic. Propositional logic doesn't have functions so it doesn't make a lot of sense to speak of unification without predicates, but with functions.
LogikalGuy 5y ago
For me the best introduction to unification was creating a microKanren[1] implementation based on the "Hello, declarative world" article[2], but even just reading the article can help enormously to understand how unification works. Basically if you have unification then you already have a simple query engine, which can handle simple equality constraints that is usually used in SQL WHERE clauses. For example "select * where pokemon = pikachu" can be simply achieved by such a system. Of course this only gives a bare bones query engine, so if you want something more advanced then you will need to implement a constraint system on top of this base unification system. cKanren is a good example of such a system. Few years ago I had the same kind a of curious question about the relationship between databases and logic programming languages like microKanren and as a result I created LogikalDB[3], which is an embedded query language for FoundationDB. 1: http://minikanren.org/ http://minikanren.org/ 2: https://codon.com/hello-declarative-world https://codon.com/hello-declarative-world 3: https://github.com/MechaRex/logikaldb https://github.com/MechaRex/logikaldb

YeGoblynQueenne 5y ago

To understand unification I recommend Robinson's seminal paper on resolution, "A machine-oriented logic based on the resolution principle", which is also referenced in your first link. It's a widely influential paper and most modern work on unification, theorem proving, logic programming etc derives from it to some extent. It's an old paper and it might look scary on first sight but it's actually pretty readable. As an aside, I'm told that Robinson's paper was in review for well over a year in a constant back-and-forth between him and referees who kept demanding improvements. Which of course was very frustrating for Robinson, but it seems to have done the job and resulted in a very readable, very clear paper. Give it a try! Btw, I'm a bit put off by the terminology chosen in your first link that treats predicates as functions. Robinson of course describes unification in first-order logic. Propositional logic doesn't have functions so it doesn't make a lot of sense to speak of unification without predicates, but with functions.

LogikalGuy 5y ago

For me the best introduction to unification was creating a microKanren[1] implementation based on the "Hello, declarative world" article[2], but even just reading the article can help enormously to understand how unification works. Basically if you have unification then you already have a simple query engine, which can handle simple equality constraints that is usually used in SQL WHERE clauses. For example "select * where pokemon = pikachu" can be simply achieved by such a system. Of course this only gives a bare bones query engine, so if you want something more advanced then you will need to implement a constraint system on top of this base unification system. cKanren is a good example of such a system. Few years ago I had the same kind a of curious question about the relationship between databases and logic programming languages like microKanren and as a result I created LogikalDB[3], which is an embedded query language for FoundationDB. 1: http://minikanren.org/ http://minikanren.org/ 2: https://codon.com/hello-declarative-world https://codon.com/hello-declarative-world 3: https://github.com/MechaRex/logikaldb https://github.com/MechaRex/logikaldb