A decidable subclass of finitary programs

TL;DR

This paper introduces FP2, a new class of logic programs that balances expressiveness and decidability, allowing infinite predicates and arbitrary arity while enabling decidable reasoning tasks.

Contribution

The paper defines FP2, a decidable subclass of finitary programs that supports infinite predicates, arbitrary arity, and stable model reasoning, addressing limitations of previous approaches.

Findings

FP2 supports predicates with infinite extensions.

Decidability of FP2 membership checking is established.

Stable model reasoning for FP2 is decidable for call-safe queries.

Abstract

Answer set programming - the most popular problem solving paradigm based on logic programs - has been recently extended to support uninterpreted function symbols. All of these approaches have some limitation. In this paper we propose a class of programs called FP2 that enjoys a different trade-off between expressiveness and complexity. FP2 programs enjoy the following unique combination of properties: (i) the ability of expressing predicates with infinite extensions; (ii) full support for predicates with arbitrary arity; (iii) decidability of FP2 membership checking; (iv) decidability of skeptical and credulous stable model reasoning for call-safe queries. Odd cycles are supported by composing FP2 programs with argument restricted programs.