Recent years have witnessed a great deal of interest in extending answer set programming with function symbols. Since the evaluation of a program with function symbols might not terminate and checking termination is undecidable, several classes of logic programs have been proposed where the use of function symbols is limited but the program evaluation is guaranteed to terminate. In this paper, we propose a novel class of logic programs whose evaluation always terminates. The proposed technique identifies terminating programs that are not captured by any of the current approaches. Our technique is based on the idea of measuring the size of terms and atoms to check whether the rule head size is bounded by the body, and performs a more fine-grained analysis than previous work. Rather than adopting an all-or-nothing approach (either we can say that the program is terminating or we cannot say anything), our technique can identify arguments that are "limited'' (i.e., where there is no infinite propagation of terms) even when the program is not entirely recognized as terminating. Identifying arguments that are limited can support the user in the problem formulation and help other techniques that use limited arguments as a starting point. Another useful feature of our approach is that it is able to leverage external information about limited arguments. We also provide results on the correctness, the complexity, and the expressivity of our technique.

Logic Program Termination Analysis Using Atom Sizes / Calautti, Marco; Greco, Sergio; Molinaro, Cristian; Trubitsyna, Irina. - (2015), pp. 2833-2839. (Intervento presentato al convegno IJCAI 15 tenutosi a Buenos Aires nel 25th-31th July 2015).

Logic Program Termination Analysis Using Atom Sizes

Marco Calautti;
2015-01-01

Abstract

Recent years have witnessed a great deal of interest in extending answer set programming with function symbols. Since the evaluation of a program with function symbols might not terminate and checking termination is undecidable, several classes of logic programs have been proposed where the use of function symbols is limited but the program evaluation is guaranteed to terminate. In this paper, we propose a novel class of logic programs whose evaluation always terminates. The proposed technique identifies terminating programs that are not captured by any of the current approaches. Our technique is based on the idea of measuring the size of terms and atoms to check whether the rule head size is bounded by the body, and performs a more fine-grained analysis than previous work. Rather than adopting an all-or-nothing approach (either we can say that the program is terminating or we cannot say anything), our technique can identify arguments that are "limited'' (i.e., where there is no infinite propagation of terms) even when the program is not entirely recognized as terminating. Identifying arguments that are limited can support the user in the problem formulation and help other techniques that use limited arguments as a starting point. Another useful feature of our approach is that it is able to leverage external information about limited arguments. We also provide results on the correctness, the complexity, and the expressivity of our technique.
2015
IJCAI 15: Proceedings of the 24th International Conference on Artificial Intelligence
Palo Alto
AAAI Press
978-1-57735-738-4
Calautti, Marco; Greco, Sergio; Molinaro, Cristian; Trubitsyna, Irina
Logic Program Termination Analysis Using Atom Sizes / Calautti, Marco; Greco, Sergio; Molinaro, Cristian; Trubitsyna, Irina. - (2015), pp. 2833-2839. (Intervento presentato al convegno IJCAI 15 tenutosi a Buenos Aires nel 25th-31th July 2015).
File in questo prodotto:
File Dimensione Formato  
C6.pdf

Solo gestori archivio

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 583.43 kB
Formato Adobe PDF
583.43 kB Adobe PDF   Visualizza/Apri

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/11572/260161
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 3
social impact