Logic: The Most General Unifier

This is my second video on logic. I will be discussing unification and the algorithm for finding the Most General Unifier (MGU).

[patricksteiner]

07:58 **Algorithm**:
Scenario: [t/u] … Given two formulas `t` and `u` we want to know if they have a MGU.
* Rule 1) if `f(t₁, …, tₙ)/f(u₁, …, uₙ)` (t and u are the same size)
then `[t₁/u₁, …, tₙ/uₙ]` (break open the equation and compare).
* Rule 2) if `g≠f` or `n≠m` in `f(t₁, …, tₙ)/g(u₁, …, uₘ)`
then FAIL (→ no MGU exists).
* Rule 3) if `X/X` (exactly the same)
then remove (them from list) and continue.
* Rule 4) if `X/f(t₁, …, tₙ)`
then `f(t₁, …, tₙ)/X` (you can switch them around).
* Rule 5) if `X ∉ (t₁, …, tₙ)` in `f(t₁, …, tₙ)/X`
then replace `X` everywhere with `f(t₁, …, tₙ)` except in `f(t₁, …, tₙ)/X`.
* Rule 6) if `X ∈ (t₁, …, tₙ)` in `f(t₁, …, tₙ)/X`
then FAIL (→ no MGU exists).

13:45 **Example**:
- [t/u] = [ q(a, g(X, a), f(Y)) / q(a, g(f(b), a), X) ]
- R1: [ a/a, g(X, a)/g(f(b), a), f(Y)/X ]
- R2: [ g(X, a)/g(f(b), a), f(Y)/X ]
- R1: [ X/f(b), a/a, f(Y)/X ]
- R4: [ f(b)/X, a/a, f(Y)/X ]
- R5: [ f(b)/X, a/a, f(Y)/f(b) ]
- R3: [ f(b)/X, f(Y)/f(b) ]
- R1: [ f(b)/X, Y/b ]
- R4: [ f(b)/X, b/Y ]
MGU = [ f(b)/X, b/Y ]

[Plumtown]

best teacher I could find, thank you.

[soaringChris]

Thank you so much! I am suffering in my Logics class at Uni because my professor is an utterly useless man. His English is extremely poor so all my brain power during his lectures is spent trying to decipher his words, all of his handouts are plagiarized Frankensteins of other textbooks. And he is never available for one-on-one meetings. Your videos are my only real hope of passing.

[michaelNXT]

Clearest explanation I could find, thank you

[dramalexi]

Thats a very clear explanation how to use that algorithm.
Now I must hope that my teacher will accept that notification.

[somesanity]

omg this was so helpful THANK YOU the first two minutes made me understand after an hour of having no idea what the fuck my question meant.. lecturer didn't explain shit. you're awesome

[WGLYYL]

Much useful than the notes I got from lecturer, thanks

[junjieyang]

Thank you so much! After listening your class, I can figure out the mgu and it's algorithm.

[rhiran]

Please Keep posting more videos on logics.. ...

[ZeekCannon]

Loved this. <3 I kind of knew unification, but the rules were always so poorly explained. This cleared it up a lot, thanks. :)

[gulshanjangid]

Thanks mate using the algorithm slide for exam today :p

[sriharshaananthoju]

how did u replace f(y) with y and f(b) with b

[niheltouil]

Thank you so much ! This is so very helpful

[drulee]

At 19:45, why can you break open the f? Why is there no rule about that listed on the page of the algorithm (13:42) ? You said because (like first rule on 13:42) both are f and have the same size (=number of arguments). But does that "breaking up" only work with functions of 1 argument? You should say that. And put it on the page about the algorithm (13:42).

[ryanlarke]

Very useful. Well explained! Thanks alot :)

[DauphinetB]

GOD. FUCKING. BLESS YOU. YOU'VE SAVED MY ASS

[igniculus_]

*KEANU REEVES* teaching unification ... This should be fun ...

[naharulhayat]

Thanks!...this is the best explanation

[shanzipanz]

This was very helpful!  Thanks so much! :)

[ZeekCannon]

At the very end, why did you swap y and b? I thought the rule only said you had to move function to left side.