Stable Models of Multi-Valued Formulas: Partial versus Total Functions

ABSTRACT. Recently, several versions of functional stable model semantics have emerged in order to express defaults involving non-Herbrand functions. We present a new perspective on these formalisms by reducing them to the General Theory of Stable Models, which allows us to understand intensional functions in terms of intensional predicates. This perspective not only allows us to transfer theoretical results established for the General Theory of Stable Models, such as safety, splitting theorem, and strong equivalence, to functional stable model semantics, but also tells us how to make further extensions, such as allowing aggregates and generalized quantifiers. In addition, we show that the functional stable model semantics that allows partial functions is no more expressive than the one that does not, in the sense that partial functions can be eliminated in favor of total functions. Based on these results, we present an implementation of different versions of functional stable model semantics by using existing ASP solvers.