OTTER's Full Sequential Algorithm

In Section we described a simplified version of OTTER's algorithm, in which no clauses are deleted from the database once they have been added. In the complete version, back subsumption tests are done on newly-derived clauses, causing deletions, and new rewrite rules may be derived in the course of the run. These new rewrite rules are immediately applied to existing clauses in the database, causing both deletions and new additions. Coping with deletions complexifies ROO since we do not want to interfere with the generation of new clauses when deleting. It turns out that this problem can be solved by having Task B handle actual deletions. Backward subsumption and backward demodulation processes can run in parallel with all other processes, but instead of actually deleting clauses from the database, they place their identifiers in shared lists where Task B (executed by only one process at a time) can find them and carry out the actual deletions. This algorithm is shown schematically in Figure .

  

Figure: Flow of Data in ROO

6#6