TY - GEN
T1 - Detecting Decidable Classes of Finitely Ground Logic Programs with Function Symbols
AU - Calautti, Marco
AU - Greco, Sergio
AU - Trubitsyna, Irina
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
U2 - 10.1145/2505879.2505883
DO - 10.1145/2505879.2505883
M3 - Conference contribution
SN - 978-1-4503-2154-9
T3 - PPDP '13
SP - 239
EP - 250
BT - Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming
PB - ACM
CY - New York, NY, USA
ER -