Backchain iteration: Towards a practical inference method that is simple enough to be proved terminating, sound, and complete

Abstract

We focus on methods for interpreting stratified datalog programs with negation, and we describe progress towards a practical, yet simple method that treats such programs as executable specifications of deductive database applications. There are simple, but inefficient inference methods that are terminating, sound and complete when used to interpret stratified logic programs without function symbols. There are also efficient, but complex implemented methods whose correctness is unknown. However, it appears that no well-known method is both efficient and simple enough to be proved terminating, sound, and complete - particularly when successive optimizations are added. Such a method should allow us to write executable specifications, at a significantly lower cost than logic programs. However, we must first close the efficiency-simplicity gap. We give a one-page abstract description of a method, called backchain iteration, and we show that it is terminating, sound, and complete on range-restricted, stratified logic specifications without function symbols. We also give an implementation of the method as a simple meta-interpreter, and we report that, on many experimental examples, it is terminating, sound, and complete and has promising efficiency. Backchain iteration interleaves backchaining from a question with forward chaining iteration. In the version described here, the distinctive characteristics are as follows. Backchaining is done reluctantly, adding new rule instances only when no new lemmas can be proved using the existing rule instances. Subquestions and rule instances are indexed by depth of backchaining. Iteration is done eagerly, to a local fixed point, using depth indexing. The pattern of backchain and iteration depends on the specification being interpreted. © 1993 Kluwer Academic Publishers.