On the Termination of Logic Programs with Function Symbols

Authors Sergio Greco, Francesca Spezzano, Irina Trubitsyna

Thumbnail PDF


  • Filesize: 489 kB
  • 11 pages

Document Identifiers

Author Details

Sergio Greco
Francesca Spezzano
Irina Trubitsyna

Cite AsGet BibTex

Sergio Greco, Francesca Spezzano, and Irina Trubitsyna. On the Termination of Logic Programs with Function Symbols. In Technical Communications of the 28th International Conference on Logic Programming (ICLP'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 17, pp. 323-333, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)


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.
  • Logic Programming
  • Function Symbols
  • Bottom-up Execution
  • Program Termination
  • Stable Models


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail