Hostname: page-component-745bb68f8f-s22k5 Total loading time: 0 Render date: 2025-02-07T01:53:22.576Z Has data issue: false hasContentIssue false

Classes of terminating logic programs

Published online by Cambridge University Press:  23 April 2002

DINO PEDRESCHI
Affiliation:
Dipartimento di Informatica, Università di Pisa, Corso Italia 40, 56125 Pisa, Italy, (e-mail: pedre@di.unipi.it, ruggieri@di.unipi.it)
SALVATORE RUGGIERI
Affiliation:
Dipartimento di Informatica, Università di Pisa, Corso Italia 40, 56125 Pisa, Italy, (e-mail: pedre@di.unipi.it, ruggieri@di.unipi.it)
JAN–GEORG SMAUS
Affiliation:
Institut für Informatik, Universität Freiburg, Georges-Köhler-Allee 52, 79110 Freiburg im Breisgau, Germany (e-mail: smaus@informatik.uni-freiburg.de)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Termination of logic programs depends critically on the selection rule, i.e. the rule that determines which atom is selected in each resolution step. In this article, we classify programs (and queries) according to the selection rules for which they terminate. This is a survey and unified view on different approaches in the literature. For each class, we present a sufficient, for most classes even necessary, criterion for determining that a program is in that class. We study six classes: a program strongly terminates if it terminates for all selection rules; a program input terminates if it terminates for selection rules which only select atoms that are sufficiently instantiated in their input positions, so that these arguments do not get instantiated any further by the unification; a program local delay terminates if it terminates for local selection rules which only select atoms that are bounded w.r.t. an appropriate level mapping; a program left-terminates if it terminates for the usual left-to-right selection rule; a program ∃-terminates if there exists a selection rule for which it terminates; finally, a program has bounded nondeterminism if it only has finitely many refutations. We propose a semantics-preserving transformation from programs with bounded nondeterminism into strongly terminating programs. Moreover, by unifying different formalisms and making appropriate assumptions, we are able to establish a formal hierarchy between the different classes.

Type
Research Article
Copyright
© 2002 Cambridge University Press