Enhancing ASP by Functions: Decidable Classes and Implementation Techniques

Abstract

This paper summarizes our line of research about the introduction of function symbols (functions) in Answer Set Programming (ASP) – a powerful language for knowledge representation and reasoning. The undecidability of reasoning on ASP with functions, implied that functions were subject to severe restrictions or disallowed at all, drastically limiting ASP applicability. We overcame most of the technical difficulties preventing this introduction, and we singled out a highly expressive class of programs with functions (FG-programs), allowing the (possibly recursive) use of function terms in the full ASP language with disjunction and negation. Reasoning on FG-programs is decidable, and they can express any computable function (causing membership in this class to be semi-decidable). We singled out also FD-programs, a subset of FG-programs which are effectively recognizable, while keeping the computability of reasoning. We implemented all results into the DLV system, thus obtaining an ASP system allowing to encode any computable function in a rich and fully declarative KRR language, ensuring termination on every FG program. Finally, we singled out the class of DFRP programs, where decidability of reasoning is guaranteed and Prolog-like functions are allowed.