Lloyd-Topor Completion and General Stable Models

TL;DR

This paper explores the connection between Lloyd-Topor program completion and Ferraris et al.'s stable model semantics, providing a theorem to characterize general stable models via first-order formulas.

Contribution

It establishes a main theorem linking Lloyd-Topor completion with general stable models, enhancing understanding of their relationship.

Findings

Main theorem characterizes stable models using first-order formulas

Uses Truszczynski's semantics for proof

Bridges Lloyd-Topor completion with modern stable model semantics

Abstract

We investigate the relationship between the generalization of program completion defined in 1984 by Lloyd and Topor and the generalization of the stable model semantics introduced recently by Ferraris et al. The main theorem can be used to characterize, in some cases, the general stable models of a logic program by a first-order formula. The proof uses Truszczynski's stable model semantics of infinitary propositional formulas.