Detecting Decidable Classes of Finitely Ground Logic Programs with Function Symbols

Marco Calautti, Sergio Greco, Irina Trubitsyna

Research output: Contribution to journalArticlepeer-review


In this article, we propose a new technique for checking whether the bottom-up evaluation of logic programs with function symbols terminates. The technique is based on the definition of mappings from arguments to strings of function symbols, representing possible values which could be taken by arguments during the bottom-up evaluation. Starting from mappings, we identify mapping-restricted arguments, a subset of limited arguments, namely arguments that take values from finite domains. Mapping-restricted programs, consisting of rules whose arguments are all mapping restricted, are terminating under the bottom-up computation, as all of its arguments take values from finite domains. We show that mappings can be computed by transforming the original program into a unary logic program: this allows us to establish decidability of checking if a program is mapping restricted. We study the complexity of the presented approach and compare it to other techniques known in the literature. We also introduce an extension of the proposed approach that is able to recognize a wider class of logic programs. The presented technique provides a significant improvement, as it can detect terminating programs not identified by other criteria proposed so far. Furthermore, it can be combined with other techniques to further enlarge the class of programs recognized as terminating under the bottom-up evaluation.
Original languageEnglish
Pages (from-to)28:1-28:42
Number of pages42
JournalACM Transactions on Computational Logic
Issue number4
Publication statusPublished - 1 Nov 2017


  • Answer set programming
  • bottom-up evaluation
  • computational complexity
  • function symbols
  • program termination
  • stable models


Dive into the research topics of 'Detecting Decidable Classes of Finitely Ground Logic Programs with Function Symbols'. Together they form a unique fingerprint.

Cite this