Prolog technology for default reasoning: proof theory and compilation techniques

The aim of this work is to show how Prolog technology can be used for effic ient implementation of query answering in default logics. The idea is to tr anslate a default theory along with a query into a Prolog program and a Pro log query such that the original query is derivable from the default theory iff the Prolog query is derivable from the Prolog program. In order to com ply with the goal-oriented proof search of this approach, we focus on defau lt theories supporting local proof procedures, as exemplified by so-called semi-monotonic default theories. Although this does not capture general def ault theories under Reiter's interpretation, it does so under alternative o nes'. For providing theoretical underpinnings, we found the resulting compilation techniques upon a top-down proof procedure based on model elimination. We show how the notion of a model elimination proof can be refined to capture default proofs and how standard techniques for implementing and improving m odel elimination theorem provers (regularity, lemmas) can be adapted and ex tended to default reasoning. This integrated approach allows us to push the concepts needed for handling defaults from the underlying calculus onto th e resulting compilation techniques. This method for default theorem proving is complemented by a model-based ap proach to incremental consistency checking. We show that the crucial task o f consistency checking can benefit from keeping models in order to restrict the attention to ultimately necessary consistency checks. This is supporte d by the concept of default lemmas that allow for an additional avoidance o f redundancy. (C) 1998 Elsevier Science B.V. All rights reserved.