Unfounded sets and well-founded semantics for general logic programs

TLDR

General logic programs are sets of rules with positive and negative subgoals, often viewed as deductive databases, and it is desirable to associate a single Herbrand model that serves as their declarative semantics for query answering. The authors introduce unfounded sets and well‑founded partial models, using them to establish the well‑founded semantics of a program. If a program’s well‑founded partial model is a full model, it is called the well‑founded model and the program is well‑behaved; this class properly contains stratified and locally stratified programs, and a program has a unique stable model exactly when it has a well‑founded model, though the converse does not hold.

Abstract

A general logic program (abbreviated to "program" hereafter) is a set of rules that have both positive and negative subgoals. It is common to view a deductive database as a general logic program consisting of rules (IDB) sitting above elementary relations (EDB, facts). It is desirable to associate one Herbrand model with a program and think of that model as the "meaning of the program," or its "declarative semantics." Ideally, queries directed to the program would be answered in accordance with this model. We introduce unfounded sets and well-founded partial models, and define the well-founded semantics of a program to be its well-founded partial model. If the well-founded partial model is in fact a model, we call it the well-founded model, and say the program is "well-behaved". We show that the class of well-behaved programs properly includes previously studied classes of "stratified" and "locally stratified" programs Gelfand and Lifschits have proposed a definition of "unique stable model" for general logic programs. We show that a program has a unique stable model if it has a well-founded model, in which case they are the same. We discuss why the converse is not true.