Unification in the context of logic programming is basically like "use these questions and solve for all the unknowns" in algebra, except it's done with logical

Unification in the context of logic programming is basically like "use these questions and solve for all the unknowns" in algebra, except it's done with logical statements instead of algebraic equations. Searching for something like "unification prolog" (Prolog being the most well-known logic programming language) will probably give helpful material. For example you could start with two facts like "Fedora is red." and "Cat is green." Then if you ask the system "X is red." it'll tell you "X = fedora". If you ask it to list all the solutions of "X and Y are not the same color." it'll list "X = fedora, Y = cat" and "X = cat, Y = fedora". This process of binding variables to values (or other variables during simplification) is unification.