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.

Detecting decidable classes of finitely ground logic programs with function symbols / M. Calautti, S. Greco, I. Trubitsyna - In: PPDP '13: Proceedings / [a cura di] R. Pena, T. Schrijvers. - New York City : ACM, 2013. - ISBN 978-1-4503-2154-9. - pp. 239-250 (( Intervento presentato al 15. convegno PPDP tenutosi a Madrid nel 2013 [10.1145/2505879.2505883].

Detecting decidable classes of finitely ground logic programs with function symbols

M. Calautti;
2013

Abstract

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.
bottom-up execution; logic programming with function symbols; program termination; stable models
Settore INF/01 - Informatica
2013
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
2505879.2505883.pdf

accesso aperto

Tipologia: Publisher's version/PDF
Dimensione 410.81 kB
Formato Adobe PDF
410.81 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/953319
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 16
  • ???jsp.display-item.citation.isi??? ND
social impact