Avoiding Non-ground Variables

For many reasoning tasks in Artificial Intelligence, it is much simpler (or even essential) to deal with ground inferences rather than with inferences comprising variables. The usual approach to guarantee ground inferences is to introduce means for enumerating the underlying Herbrand-universe so that during subsequent inferences variables become bound in turn to the respective Herbrand-terms. The inherent problem with such an approach is that it may cause a tremendous number of unnecessary backtracking steps due to heaps of incorrect variable instantiations. In this paper, we propose a new concept that refrains from backtracking by appeal to novel inference rules that allow for correcting previous variable bindings. We show that our approach is not only beneficial for classical proof systems but it is also well-suited for tasks in knowledge representation and reasoning. The major contribution of this paper lies actually in an application of our approach to a calculi conceived for reasoning with default logic.