Detecting Optimal Termination Conditions of Logic Programs - Université de La Réunion Accéder directement au contenu
Communication Dans Un Congrès Année : 2002

Detecting Optimal Termination Conditions of Logic Programs

Résumé

In this paper, we begin with 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 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. An experimental evaluation is reported. 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.
Fichier principal
Vignette du fichier
Detecting_optimal_termination_conditions_of_logic_programs.pdf (207.35 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01915746 , version 1 (08-11-2018)

Identifiants

  • HAL Id : hal-01915746 , version 1

Citer

Frédéric Mesnard, Etienne Payet, Ulrich Neumerkel. Detecting Optimal Termination Conditions of Logic Programs. 9th International Static Analysis Symposium (SAS 2002), Sep 2002, Madrid, Spain. pp.509-525. ⟨hal-01915746⟩
34 Consultations
146 Téléchargements

Partager

Gmail Facebook X LinkedIn More