<< Prev | - Up - |
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.
<< Prev | - Up - |