The agenda method is based on a priority queue. The elements in the queue are ordered relative to their assigned priorities, where the task with the highest priority is at the front of the queue and the one with the smallest is at the back. Using this mechanism it is very easy to realize a depth-first or breadth-first strategy. Suppose that we maintain a counter LemmaCounter that enumerates the stored lemmas starting from one. Directly using the value of this counter realizes a depth-first strategy, since each new task is added to the front of the queue. Using its negation instead would realize a breadth-first strategy, because processing of new items is delayed until older tasks are processed.
The advantage of a depth-first strategy is that in the case only the first result should be computed the number of items added to the table S is less than the number of generated items added to the agenda. Since, only in the case an item is added to the table the blocking rule is applied, the subsumption operation need only be performed on a subset of the items stored in the agenda. This means, that although our inference rules exhibit a breadth-first component, using an agenda mechanism restricts the computional overhead of subsumption on that set of items that are used in specific situations, e.g., depth-first and best-first strategies.
In addition to a depth-first and breadth-first task-selection function, we have also defined a definition for PRIO where the priority is determined randomly using a built in function RANDOM, because all three priority functions together characterize a representative degree of possible agenda strategies.
However, it would also be possible, to use more complex priority functions as for instance the one proposed in [Shieber1988]). This would open up the realization of some psychologically interesting strategies (like garden-path phenomena, minimal attachment phenomena, or more general preference based strategies, see [Kay1986, Shieber1988, Görz1988, Shieber1989, Erbach1991]), however using the same deductive approach. It should be clear, that our specification is open to such more sophisticated use of priority functions.