So, how do Prolog programs work then?

• Given a program and a query, one wants to know if the program can satisfy the query.
• Based on the resolution principle, at the heart of which lies the process of unification

Unification

Given 2 terms A and B, determine whether they are equal (not necessarily identical, but involving assignment of values to variables).

• if A and B are constant, then they match if and only if they are identical
• If A is a variable and B anything else, theny they match by A becoming instantiated to B. Similarly, if A is anything and B is a variable.
• if A and B are compound terms, then they match if they have the same main functor (arity must be the same) ;
  - all their corresponding components match in a pair wise manner, by reapplying the algorithm