Enriching Datalog programs with function symbols makes modeling easier, increases the expressive power, and allows us to deal with infinite domains. However, this comes at a cost: common inference tasks become undecidable. To cope with this issue, recent research has focused on finding trade-offs between expressivity and decidability by identifying classes of logic programs that impose limitations on the use of function symbols but guarantee decidability of common inference tasks. Despite the significant body of work in this area, current approaches do not include many simple practical programs whose evaluation terminates. In this paper, we present the novel class of rule-bounded programs. While current techniques perform a limited analysis of how terms are propagated from an individual argument to another, our technique is able to perform a more global analysis, thereby overcoming several limitations of current approaches. We show different results on the correctness and the expressivity of the proposed technique.

Checking Termination of Datalog with Function Symbols Through Linear Constraints / Calautti, Marco; Greco, Sergio; Molinaro, Cristian; Trubitsyna, Irina. - (2015), pp. 192-199. (Intervento presentato al convegno SEBD tenutosi a Gaeta nel 14th -17th June 2015).

Checking Termination of Datalog with Function Symbols Through Linear Constraints

Marco Calautti;
2015-01-01

Abstract

Enriching Datalog programs with function symbols makes modeling easier, increases the expressive power, and allows us to deal with infinite domains. However, this comes at a cost: common inference tasks become undecidable. To cope with this issue, recent research has focused on finding trade-offs between expressivity and decidability by identifying classes of logic programs that impose limitations on the use of function symbols but guarantee decidability of common inference tasks. Despite the significant body of work in this area, current approaches do not include many simple practical programs whose evaluation terminates. In this paper, we present the novel class of rule-bounded programs. While current techniques perform a limited analysis of how terms are propagated from an individual argument to another, our technique is able to perform a more global analysis, thereby overcoming several limitations of current approaches. We show different results on the correctness and the expressivity of the proposed technique.
2015
23rd Italian Symposium on Advanced Database Systems, SEBD 2015,Gaeta, Italy, June 14-17, 2015
Red Hook, New York
Curran Associates, Inc.
978-151081087-7
Calautti, Marco; Greco, Sergio; Molinaro, Cristian; Trubitsyna, Irina
Checking Termination of Datalog with Function Symbols Through Linear Constraints / Calautti, Marco; Greco, Sergio; Molinaro, Cristian; Trubitsyna, Irina. - (2015), pp. 192-199. (Intervento presentato al convegno SEBD tenutosi a Gaeta nel 14th -17th June 2015).
File in questo prodotto:
File Dimensione Formato  
C4.pdf

Solo gestori archivio

Tipologia: Post-print referato (Refereed author’s manuscript)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 272.8 kB
Formato Adobe PDF
272.8 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/260181
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact