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