Basic Knowledge: Unification

Unification is the process for setting values from one literal into the variables of another literal, e.g. determining the current value of Colour in light(Colour). Note: Colour is a variable! Based on the previous → time example the procedure can look as follows:

We have two literals, one literal with values and another literal with variables

time( current( hour( 2    ), minute( 0      ), period( pm()   ) ) )
time( current( hour( Hour ), minute( Minute ), period( Period ) ) )

Based on this structure the systems tries to transfer the values from the first literal into the variables of the second literal, such that both literals are equal. If it is not possible the unification process will fail. During a successful execution, the variable Hour stores the number $2$, the variable Minute the number $0$ and the variable Period the → atom pm.

The runtime of the logic programming language tries to find an executable structure so that all unification components and → rules can be finished successfully. The unification process can be used to generate new literals based on existing literals. In combination with rules the system can solve complex reasoning structures. If the system cannot find any possibility to solve the problem, the logic program will be stopped with a failure. The goal of the runtime is to find a successful solution.

In AgentSpeak(L++) unification can be done by using the right shift operator >> in combination with a literal to be unified. → Terms of interest are then replaced by → variables.

As unification provides values for the first matching literal in the belief base (not necessarily in denoted order), applying constraints can be quite helpful to get the literal of interest. It is therefore possible to provide certain logical constraints to variables, by using the

>>(literal, constraint)

Examples

We want to get the current values of the complex literal

time( current( hour( 2 ), minute( 0 ), period( pm() ) ) )

but are not interested in the value of the period. Nevertheless we will have to provide the complete literal to the unification:

>>time( current( hour( Hour ), minute( Minute ), period( _ ) ) )

which unifies Hour and Minute to 2 and 0 respectively. For the value of the period we will also have to provide a variable. Here we can use the variable _ as placeholder.

As unification provides values for the first match, applying constraints can be helpful. Consider the three beliefs

periods( am(), pm() ).
time( current( hour( 10 ), minute( 0  ), period( am() ) ) ).
time( current( hour( 4  ), minute( 30 ), period( pm() ) ) ).

in Bob’s belief base, describing the two periods a day can have and two appointments he has.
Alice would like to know whether Bob has an appointment after 4 o’clock in the afternoon. To get only the values of the second time(…) belief, Bob could unify the values as follows (as he already knows two constraints, provided by Alice):

>>periods(AM, PM);  // unify possible periods into variables AM and PM to use them in the unification below
>>( time( current( hour( Hour ), minute( Minute ), period( Period ) ) ), Period == PM && Hour >= 4);

This will yield 4, 30, and pm for Hour, Minute and Period respectively.