5.2.2 Inferential Closure Algorithm

We now outline at a fairly abstract level an algorithm for computing the inferential closure of a set of Literals, given a set of inference rules. Given a literal X and an inference rule R, we write R(X) for the set of literals which can be derived by applying R to X. Our first algorithm is:

• pick an element X of Literals

• pick an inference rule R

• add R(X) to Literals

• repeat until no new literal can be added

We can improve on this algorithm by distinguishing between literals which have already been processed (i. e. cannot contribute new conclusions) and those which are yet unprocessed. Thus, we distinguish two sets of literals: DONE and TODO. Our second algorithm is:

• initially set DONE to empty and TODO to Literals.

• while TODO is not empty:

  • remove an element X from TODO

  • add X to DONE

  • for each rule R, add R(X) to TODO

The datastructure used to implement TODO is often called an agenda. It is typically either a stack or a queue.