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).

[@patricksteiner3859]

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 ]

[@junjieyang3444]

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

[@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.

[@noel2071]

have you passed it though?

[@I3uzzzzzz]

@@noel2071 he became homeless and died

[@michaelNXT1]

Clearest explanation I could find, thank you

[@ZeekCannon]

Loved this.

[@ryanlarke2618]

Very useful. Well explained! Thanks alot :)

[@baharehbadiei7698]

Thanks a lot Raoul. Very helpful.

[@shanzipanz]

This was very helpful! Thanks so much! :)

[@dramalexi]

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

[@WGLYYL01]

Much useful than the notes I got from lecturer, thanks

[@lala-jy4kz]

Excellent introduction!

[@user-il6ob8lw1m]

Great explanation! Thanks

[@ShaiTeller]

Thanks a lot mate, really helpful.

[@niheltouil7513]

Thank you so much ! This is so very helpful

[@luca8932]

Thanks voor de uitleg!

[@naharulhayat]

Thanks!...this is the best explanation

[@wpunkthenry]

Thank you Raoul!

[@yunhanli8159]

Good explanation, thank you

[@RituRajdps]

thanx mate. that was really helpful

[@uzoosiona1588]

thank you so much ....really helpful

[@rhiran8924]

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

[@kuzaxe]

Thanks Raoul!

[@cpriyankara]

good explanation, thanks!

[@gulshanjangid3470]

Thanks mate using the algorithm slide for exam today :p

[@somesanity1]

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

[@user-assia]

thank you that was very useful :)

[@Benny1196]

Thank you very much :)

[@hariminggu7205]

nice video, thank you so much, it's very helpful! :)

[@fufuhu148]

very good

[@harish261000]

good explanation

[@giladeini]

thanks, was realy good

[@radhouanebenbrahim1661]

thank you

[@AwsomeAlligator]

Thanks for the great explanation, but those unmatched parentheses are bothering my pseudo-ocd :D

[@igniculus_]

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

[@SgtKanyo]

Dude it's young Jake Gyllenhaal

[@Poncholay]

Saved me a headache

[@DauphinetB]

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

[@sriharshaananthoju8671]

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

[@marshaul]

You might consider crossing your Zs. They look like 2s to me. =)

[@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.

[@MagicTheGabriel]

+Elijah Kohrt you have to move everything to the left side that is not a variable. and a and b are constants.

[@dramalexi]

+Elijah Kohrt
Because you cannot just replace the b in f(b) with the y in [f(b) / x, y/b]
You have to swap the b to the left side to [f(b) / x, b/y] before you can substitute. That is as I understood the algorithm.

[@ZeekCannon]

Yeah it's been a while, but I think I just didnt get that a and b were constants. Thanks. :)

[@IslamHanafieh]

thanks for the nice video,
but i still cant understand it !!
in my book it says that if the first variable equals the second, there will be no MGU !!
but in the second example you did that at 03:08 there was (a) at both of the tow formula !!
here's some question i got at home exam, can you please help me with !!?
1. f(g(w),h) , f(g(b),h).
2. likes(r,t) , likes(t,r).
3. shape(ball,round) , shape(Z,A).
4. power(M,2) , power(N).
5. div(X,7) , div(5,3).
6. aunt(F,L) , aunt(Helen,helen)
thanks

[@xamidi]

0:43 rightmost parenthesis is missing

[@AntoniaIvanovaStorm]

thanks hotty

[@soccerfp]

no problem

[@drulee3000]

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).

[@ZeekCannon]

+drulee3000 In general when people write x_1,... x_n, then when n=1, we just have x_1.
So there is a rule listed.

[@hakiterror9274]

u look like tom odell lol

[@savassemirli3539]

OMG! I'm sorry but you sound EXACTLY like a young Walter Lewin! 🤩

[@Stefan06091991]

U are a champ! Our lecturer is useless, nowhere near as informative as this ...