Detecting Decidable Classes of Finitely Ground Logic Programs with Function Symbols

Marco Calautti, Sergio Greco, Irina Trubitsyna

Research output: Chapter in Book/Report/Conference proceedingConference contribution


In this paper 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. Such mappings can be computed by transforming the original program into a unary logic program whose termination is decidable. Starting from mappings we can identify mapping-restricted arguments, a subset of limited arguments, that is, arguments which can take values from finite domains. The class of mapping-restricted programs, consisting of programs whose arguments are mapping-restricted, is terminating under the bottom-up computation as all its arguments can take values from finite domains. We study the complexity of the presented approach and compare it with other techniques known in the literature. The presented technique is relevant as it individuates as terminating programs not detected by other criteria proposed so far and can be combined with other techniques to further enlarge the class of programs recognized as terminating under the bottom-up evaluation.
Original languageEnglish
Title of host publicationProceedings of the 15th Symposium on Principles and Practice of Declarative Programming
Place of PublicationNew York, NY, USA
Number of pages12
ISBN (Print)978-1-4503-2154-9
Publication statusPublished - 2013

Publication series

NamePPDP '13

Cite this