Enriching answer set programming 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 also present a further class of cycle-bounded programs where groups of rules are analyzed together. We show different results on the correctness and the expressivity of the proposed techniques.
Checking Termination of Logic Programs with Function Symbols through Linear Constraints / M. Calautti, S. Greco, C. Molinaro, I. Trubitsyna (LECTURE NOTES IN COMPUTER SCIENCE). - In: Rules on the Web: From Theory to Applications / [a cura di] A. Bikakis, P. Fodor, D. Roman. - [s.l] : Springer, 2014. - ISBN 978-3-319-09869-2. - pp. 97-111 (( convegno 8th International Symposium, RuleML 2014, Co-located with the 21st European Conference on Artificial Intelligence, ECAI 2014 tenutosi a Praha nel 2014 [10.1007/978-3-319-09870-8_7].
Checking Termination of Logic Programs with Function Symbols through Linear Constraints
M. Calautti;
2014
Abstract
Enriching answer set programming 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 also present a further class of cycle-bounded programs where groups of rules are analyzed together. We show different results on the correctness and the expressivity of the proposed techniques.File | Dimensione | Formato | |
---|---|---|---|
978-3-319-09870-8_7.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
301.65 kB
Formato
Adobe PDF
|
301.65 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.