The Resolvent

The term resolvent originates from Logic Programming. It is the set of all goals that need to be satisfied. The computation typically starts with a top-level goal, then gets successively transformed (by substituting goals that match a clause head with an instance of the clause body, ie. a sequence of sub-goals), and eventually terminates with one of the trivial goals true or fail. For example, given the program

p :- q,r.
q.
r :- q.

and the goal p, the resolvent goes through the following states before the goal is proven and the computation terminates:

p ----> q,r ----> r ----> q ----> {}

While in Prolog the resolvent is always processed from left to right, the resolvent in ECLiPSe is more structured, and can be manipulated in a much more flexible way. This is achieved by two basic mechanisms, suspension and priorities.

Suspended goals form the part of the resolvent which is currently not being considered. This is typically done when we know that we cannot currently infer any interesting information from them.

The remaining goals are ordered according to their priority. At any time, the system attempts to solve the most urgent subgoal first. ECLiPSe currently supports a fixed range of 12 different priorities, priority 1 being the most urgent and 12 the least urgent.

Figure 17.1 shows the structure of the resolvent. When a toplevel goal is launched, it has priority 12 and is the only member of the resolvent. As execution proceeds, active goals may be suspended, and suspended goals may be woken and scheduled with a particular priority.

Figure 17.1: Structure of the resolvent