A NON-GROUND REALIZATION OF THE STABLE AND WELL-FOUNDED SEMANTICS

The declarative semantics of nonmonotonic logic programming has largel y been based on propositional programs. However, the ground instantiat ion of a logic program may be very large, and likewise, a ground stabl e model may also be very large. We develop a non-ground semantic theor y for non-monotonic logic programming. Its principal advantage is that stable models and well-founded models call be represented as sets of atoms, rather than as sets of ground atoms, A set SI of atoms may be v iewed as a compact representation of the Herbrand interpretation consi sting of all ground instances of atoms in SI. We develop generalizatio ns of the stable and well-founded semantics based on such non-ground i nterpretations SI. The key notions for our theory are those of covers and anticovers. A cover as well as its anticover are sets of substitut ions - non-ground in general - representing all substitutions obtained by ground instantiating some substitution in the (anti)cover, with th e additional requirement that each ground substitution is represented either by the cover or by the anticover, but not by both. We develop m ethods for computing anticovers for a given cover, show that membershi p in so-called optimal covers is decidable, and investigate the comple xity in the Datalog case.