Atoms

Any non-reserved lowercase word represents an entity, or unique item, in our universe of interest, e.g. x, foo, fred, green, etc.

Variables

Any uppercase word designates a variable, e.g. X, Foo, SomeValue, etc.

When first created, variables do not have a value or data type associated with them, and are said to be uninstantiated. Once a variable is assigned a value the variable is said to be instantiated. Instantiation is the act of associating a specific value with a variable.

When two variables refer to the same actual entity (not just equal values) they are said to be unified. (Unification is the act of making two variables refer to the same entity.)

If you want a variable to act as a placeholder but you don't care what the actual value is, you can use the underscore, _, as an anonymous variable. (We'll see many uses for this later.) If you want to provide a name rather than just _ to make the code more readable, you can use _ followed by the desired name, e.g. _Tail.

is versus = versus ==

"is" acts like assignment, the item on the RHS must work out to an appropriate value, while the item on the LHS must be an uninstantiated variable
e.g. X is 3. succeeds if X doesn't already have a value.

"=" unifies two variables, e.g. X=Y means X and Y are now treated as the same item. If one of them was already instantiated then both are now instantiated. If both of them were already instantiated with different things then the attempted unification will fail.

Equality tests
There are a number of forms of equality/inequality testing in Prolog, the "\" versions are the negated forms:

• X =:= Y, X =\= Y Numeric Equality: true iff X and Y evaluate to equivalent numbers (=\= for not equivalent)
• X == Y, X \== Y Equivalence: X == Y is true iff X and Y are equivalent terms (\== for not-equivalent)
• X = Y, X \= Y Unification: true iff X and Y can be unified (\= for cannot unify)
• \+ (TERM) Not proven: true if the prolog engine cannot find a way to make TERM true, false otherwise. This is not necessarily the same as boolean NOT.
  An interesting side note is that \+(\+(A=B)) will tell you if A is unifiable with B but will not have the effect of actually unifying them.
  The syntax not(TERM) is also supported, but means the same thing as \+, i.e. not(TERM) is true if the term cannot be proven true, and is false if the term can be proven true.