Non-Termination Inference for Optimal Ter-mination Conditions of Logic Programs

Abstract : In this paper, we present an approach to non-termination inference of logic programs. Our framework relies on an extension of the Lifting Theorem, where some specific argument positions can be instantiated while others are generalized. Atomic left looping queries are then generated bottom-up from selected subsets of the binary unfoldings of the program of interest. Then non-termination inference is tailored to attempt proofs of optimality of left termination conditions computed by a termination inference tool. For each class of atomic queries not covered by a termination condition, the aim is to ensure the existence of one query from this class which leads to an infinite search tree. When termination and non-termination analysis produce complementary results for a logic procedure , they induce a characterization of the operational behavior of the logic procedure with respect to the left most selection rule and the language used to describe sets of atomic queries.
Document type :
Conference papers
Complete list of metadatas

Cited literature [19 references]  Display  Hide  Download

http://hal.univ-reunion.fr/hal-01915407
Contributor : Réunion Univ <>
Submitted on : Wednesday, November 7, 2018 - 3:41:33 PM
Last modification on : Thursday, March 28, 2019 - 11:24:11 AM
Long-term archiving on : Friday, February 8, 2019 - 3:39:11 PM

File

Non_termination_inference_for_...
Explicit agreement for this submission

Identifiers

  • HAL Id : hal-01915407, version 1

Collections

Citation

Frédéric Mesnard, Etienne Payet, Ulrich Neumerkel. Non-Termination Inference for Optimal Ter-mination Conditions of Logic Programs. 11èmes Journées Francophones de Programmation en Logique et Programmation par Contraintes (JFPLC'02), Association Française pour la Programmation en Logique et la programmation par Contraintes (AFPLC), May 2002, Nice, France. pp.84-104. ⟨hal-01915407⟩

Share

Metrics

Record views

18

Files downloads

5