Termination Analysis for Abductive General Logic Programs
Sofie Verbaeten · The MIT Press eBooks · 1999
Introduction Proving termination of programs is important in any approach to program development. In this paper, we address the termination behaviour of abductive general logic programs and queries. Abduction is a form of reasoning which, given a knowledge base and an observation Q, nds possible explanations of Q in terms of a particular set of predicates, called the abducible predicates. In the context of logic programming, abductive procedures have been used for planning, knowledge assimilation and belief revision, database updating, reasoning in the context of temporal domains with uncertainty, . . . (we refer to [7] for references to such works). In [7], Denecker and De Schreye present an abductive extension of SLDNF [1], called SLDNFA. We study termination of general logic programs executed under SLDNFA w.r.t. an arbitrary safe selection rule. We show that the termination conditions for SLDNF of Apt and Bezem [3], namely acyclicity of the