Computing Stable Models of Normal Logic Programs Without Grounding

TL;DR

This paper introduces a novel method for computing stable models of normal logic programs with complex terms and negation, avoiding the need for grounding and enabling direct execution under stable model semantics.

Contribution

It presents a groundless, direct execution approach for normal logic programs with complex data structures, using non-Herbrand universe and coinduction techniques.

Findings

Successfully computes stable models without grounding

Supports complex data structures like lists

Prototype demonstrates practical feasibility

Abstract

We present a method for computing stable models of normal logic programs, i.e., logic programs extended with negation, in the presence of predicates with arbitrary terms. Such programs need not have a finite grounding, so traditional methods do not apply. Our method relies on the use of a non-Herbrand universe, as well as coinduction, constructive negation and a number of other novel techniques. Using our method, a normal logic program with predicates can be executed directly under the stable model semantics without requiring it to be grounded either before or during execution and without requiring that its variables range over a finite domain. As a result, our method is quite general and supports the use of terms as arguments, including lists and complex data structures. A prototype implementation and non-trivial applications have been developed to demonstrate the feasibility of our method.