License: Creative Commons Attribution-NoDerivs 3.0 Unported license (CC BY-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICLP.2012.323
URN: urn:nbn:de:0030-drops-36335
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3633/
Go to the corresponding LIPIcs Volume Portal

Greco, Sergio ; Spezzano, Francesca ; Trubitsyna, Irina

On the Termination of Logic Programs with Function Symbols

pdf-format:
31.pdf (0.5 MB)

Abstract

Recently there has been an increasing interest in the bottom-up evaluation of the semantics of logic programs with complex terms. The main problem due to the presence of functional symbols in the head of rules is that the corresponding ground program could be infinite and that finiteness of models and termination of the evaluation procedure is not guaranteed. This paper introduces, by deeply analyzing program structure, new decidable criteria, called safety and Gamma-acyclicity,
for checking termination of logic programs with function symbols under bottom-up evaluation. These criteria guarantee that stable models are finite and computable, as it is possible to generate
a finitely ground program equivalent to the source program. We compare new criteria with other decidable criteria known in the literature and show that the Gamma-acyclicity criterion is the most
general one. We also discuss its application in answering bound queries.

BibTeX - Entry

@InProceedings{greco_et_al:LIPIcs:2012:3633,
  author =	{Sergio Greco and Francesca Spezzano and Irina Trubitsyna},
  title =	{{On the Termination of Logic Programs with Function Symbols}},
  booktitle =	{Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)},
  pages =	{323--333},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-43-9},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{17},
  editor =	{Agostino Dovier and V{\'i}tor Santos Costa},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3633},
  URN =		{urn:nbn:de:0030-drops-36335},
  doi =		{10.4230/LIPIcs.ICLP.2012.323},
  annote =	{Keywords: Logic Programming, Function Symbols, Bottom-up Execution, Program Termination, Stable Models}
}

Keywords: Logic Programming, Function Symbols, Bottom-up Execution, Program Termination, Stable Models
Collection: Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)
Issue Date: 2012
Date of publication: 05.09.2012

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI