Automata and answer set programming

Abstract

In answer set programming (ASP), one does not allow the use of function symbols. Disallowing function symbols avoids the problem of having logic programs which have stable models of excessively high complexity. For example, Marek, Nerode, and Remmel showed that there exist finite predicate logic programs which have stable models but which have no hyperarithmetic stable model. Of course, by eliminating function symbols, one loses a lot of expressive power in the language. In particular, it is difficult to directly reason about infinite sets in ASP. Blair, Marek, and Remmel [BMR08] developed an extension of logic programming called set based logic programming. In the theory of set based logic programming, the atoms represent subsets of a fixed universe X and one is allowed to compose the one-step consequence operator with a monotonic idempotent operator O so as to ensure that the analogue of stable models are always closed under O. We show that if the sets represented by the atoms in a finite set based program P are languages accepted by finite automaton, and the operators involved in the construction have a certain natural property, then all the stable models of P are languages accepted by finite automaton and one can effectively check whether a language accepted by a finite automaton is a stable model of the set based logic program. Thus in this setting, one can effectively reason about certain classes of infinite sets. © Springer-Verlag Berlin Heidelberg 2009.