Report Number: CS-TR-96-1572
Institution: Stanford University, Department of Computer Science
Title: Caching and Non-Horn Inference in Model Elimination Theorem
Provers
Author: Geddis, Donald F.
Date: June 1996
Abstract: Caching in an inference procedure holds the promise of
replacing exponential search with constant-time lookup, at a
cost of slightly-increased overhead for each node expansion.
Caching will be useful if subgoals are repeated often enough
during proofs.
In experiments on solving queries using a backward chainer on
Horn theories, caching appears to be very helpful on average.
When trying to extend this success to first-order theories,
however, intuition suggests that subgoal caches are no longer
useful. The cause is that complete first-order backward
chaining requires goal-goal resolutions in addition to
resolutions with the database, and this introduces a
context-sensitivity into the proofs for a subgoal. A cache is
only feasible if the solutions are independent of context, so
that they may be copied from one part of the space to
another.
It is shown here that a full exploration of a subgoal in one
context actually provides complete information about the
solutions to the same subgoal in all other contexts of the
proof. In a straightforward way, individual solutions from
one context may be copied over directly. More importantly,
non-Horn failure caching is also feasible, so no additional
solutions in the new context (that might affect the query)
are possible and therefore there is no need to re-explore the
space in the new context. Thus most Horn clause caching
schemes may be used with minimal changes in a non-Horn
setting.
In addition, a new Horn clause caching scheme is proposed:
postponement caching. This new scheme involves exploring the
inference space as a graph instead of as a tree, so that a
given literal will only occur once in the proof space.
Despite the previous extension of failure caching to non-Horn
theories, postponement caching is incomplete in the non-Horn
case. A counterexample is presented, and possible
enhancements to reclaim completeness are investigated.
http://i.stanford.edu/pub/cstr/reports/cs/tr/96/1572/CS-TR-96-1572.pdf