Answer set computation based on a minimal model generation theorem prover

Abstract

Answer set programming (ASP) has been a focus as a new declarative programming paradigm. The basic algorithm to compute answer sets based on a model generation theorem proving scheme has been proposed by Inoue [7]. The implementation of the basic algorithm, however, generates enormous redundant combinations of hypotheses. In this paper, we propose a new implementation method based on a minimal model generator MM-MGTP [5], including a new data structure called modal disjunction buffer and some extended operations to avoid redundancy. Some experimental results are shown for comparison with the naive implementation and other systems. © Springer-Verlag Berlin Heidelberg 2004.