Nontermination inference of logic programs

17Citations
Citations of this article
6Readers
Mendeley users who have this article in their library.

Abstract

We present a static analysis technique for nontermination inference of logic programs. Our framework relies on an extension of the subsumption test, where some specific argument positions can be instantiated while others are generalized. We give syntactic criteria to statically identify such argument positions from the text of a program. Atomic left looping queries are generated bottom-up from selected subsets of the binary unfoldings of the program of interest. We propose a set of correct algorithms for automating the approach. Then, nontermination inference is tailored to attempt proofs of optimality of left termination conditions computed by a termination inference tool. An experimental evaluation is reported and the analyzers can be tried online at http://www.univ-reunion.fr/~gcc. When termination and nontermination analysis produce complementary results for a logic procedure, then with respect to the leftmost selection rule and the language used to describe sets of atomic queries, each analysis is optimal and together, they induce a characterization of the operational behavior of the logic procedure. © 2006 ACM.

Cite

CITATION STYLE

APA

Payet, E., & Mesnard, F. (2006). Nontermination inference of logic programs. ACM Transactions on Programming Languages and Systems, 28(2), 256–289. https://doi.org/10.1145/1119479.1119481

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free