Comments on unification

Here is a synopsis of how the unification algorithm works on different combinations of arguments. The rows in the table indicate the arguments for one predicate, the columns indicate the arguments for the other. The notation (x/y) indicates that x is substituted by y.

constantvariablefunction
constantSUCCESS if constants are the same, FAIL otherwise {variable/constant} FAIL
variable{variable/constant} {variable/variable} {variable/function} if variable does not occur in function, FAIL otherwise
function FAIL {variable/function} if variable does not occur in function, FAIL otherwise the result of unifying the arguments if the functions are the same and the arguments unify, FAIL otherwise

Examples

In the following examples we are interested just in unification, not in resolution.