Logic: The Most General Unifier

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

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

[@dramalexi]

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

[@rhiran8924]

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

[@junjieyang3444]

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

[@lala-jy4kz]

Excellent introduction!

[@WGLYYL01]

Much useful than the notes I got from lecturer, thanks

[@baharehbadiei7698]

Thanks a lot Raoul. Very helpful.

[@igniculus_]

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

[@SgtKanyo]

Dude it's young Jake Gyllenhaal

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

[@luca8932]

Thanks voor de uitleg!

[@xamidi]

0:43 rightmost parenthesis is missing

[@niheltouil7513]

Thank you so much ! This is so very helpful

[@ZeekCannon]

Loved this.

[@naharulhayat]

Thanks!...this is the best explanation

[@wpunkthenry]

Thank you Raoul!

[@ryanlarke2618]

Very useful. Well explained! Thanks alot :)

[@영어이야기]

Great explanation! Thanks

[@sriharshaananthoju8671]

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

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

[@gulshanjangid3470]

Thanks mate using the algorithm slide for exam today :p

[@DauphinetB]

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

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

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

[@marshaul]

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

[@ShaiTeller]

Thanks a lot mate, really helpful.

[@RituRajdps]

thanx mate. that was really helpful

[@AwsomeAlligator]

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

[@shanzipanz]

This was very helpful! Thanks so much! :)

[@yunhanli8159]

Good explanation, thank you

[@kuzaxe]

Thanks Raoul!

[@uzoosiona1588]

thank you so much ....really helpful

[@cpriyankara]

good explanation, thanks!

[@harish261000]

good explanation

[@Poncholay]

Saved me a headache

[@fufuhu148]

very good

[@user-assia]

thank you that was very useful :)

[@Benny1196]

Thank you very much :)

[@hariminggu7205]

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

[@giladeini]

thanks, was realy good

[@radhouanebenbrahim1661]

thank you

[@AntoniaIvanovaStorm]

thanks hotty

[@soccerfp]

no problem

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

[@hakiterror9274]

u look like tom odell lol