Abstract machine for efficiently computing queries to well-founded models

The well-founded semantics has gained wide acceptance partly because it is a skeptical semantics. That is, the well-founded model posits as unknown atoms which are deemed true or false in other formalisms such as stable models. This skepticism makes the well-founded model not only useful in itself, but also suitable as a basis for other forms of non-monotonic reasoning. For instance, since algorithms to compute stable models are intractable, the atoms relevant to such algorithms can be limited to those undefined in the well-founded model. Thus, an engine that efficiently evaluates programs according to the well-founded semantics can be seen as a prerequisite to practical systems for non-monotonic reasoning. This paper describes the architecture of the Warren Abstract Machine (WAM)-based abstract machine underlying the XSB system. This abstract machine, called the SLG-WAM, uses tabling to efficiently compute the well-founded semantics of non-ground normal logic programs in a goal-directed way. To do so, the SLG-WAM requires sophisticated extensions to its core tabling engine for fixed-order stratified programs. A mechanism must be implemented to represent answers that are neither true nor false, and the delay and simplification operations - which serve to break and to resolve cycles through negation, must be implemented. We describe fully these extensions to our tabling engine, and demonstrate the efficiency of our implementation in two ways. First, we present a theorem that bounds the need for delay to those literals which are not dynamically stratified for a fixed-order computation. Second, we present performance results that indicate that the overhead of delay and simplification to Prolog-or tabled-evaluations is minimal.