Fages' Theorem and Answer Set Programming

TL;DR

This paper generalizes Fages' theorem to clarify when the completion semantics and answer set semantics coincide, enabling answer sets to be computed via satisfiability solvers, thus impacting answer set programming practice.

Contribution

It extends Fages' theorem to broader classes of logic programs, linking completion and answer set semantics, facilitating the use of SAT solvers in answer set programming.

Findings

Semantics equivalence allows SAT-based answer set computation

Logic programming blocks world example illustrates the theorem

Generalization broadens applicability of answer set solvers

Abstract

We generalize a theorem by Francois Fages that describes the relationship between the completion semantics and the answer set semantics for logic programs with negation as failure. The study of this relationship is important in connection with the emergence of answer set programming. Whenever the two semantics are equivalent, answer sets can be computed by a satisfiability solver, and the use of answer set solvers such as smodels and dlv is unnecessary. A logic programming representation of the blocks world due to Ilkka Niemelae is discussed as an example.