Unfolding Partiality and Disjunctions in Stable Model Semantics

TL;DR

This paper presents a methodology to implement partial and disjunctive stable models by unfolding them into normal stable models, enabling the use of existing stable model solvers and demonstrating practical system performance.

Contribution

It introduces a novel unfolding approach that transforms partial and disjunctive stable models into normal stable models, facilitating their implementation with existing tools.

Findings

Successfully implemented a system for disjunctive stable models using smodels.

Compared system performance with the DLV system, showing competitive results.

Demonstrated the feasibility of the unfolding approach for practical applications.

Abstract

The paper studies an implementation methodology for partial and disjunctive stable models where partiality and disjunctions are unfolded from a logic program so that an implementation of stable models for normal (disjunction-free) programs can be used as the core inference engine. The unfolding is done in two separate steps. Firstly, it is shown that partial stable models can be captured by total stable models using a simple linear and modular program transformation. Hence, reasoning tasks concerning partial stable models can be solved using an implementation of total stable models. Disjunctive partial stable models have been lacking implementations which now become available as the translation handles also the disjunctive case. Secondly, it is shown how total stable models of disjunctive programs can be determined by computing stable models for normal programs. Hence, an implementation of stable models of normal programs can be used as a core engine for implementing disjunctive programs. The feasibility of the approach is demonstrated by constructing a system for computing stable models of disjunctive programs using the smodels system as the core engine. The performance of the resulting system is compared to that of dlv which is a state-of-the-art special purpose system for disjunctive programs.