| Home > Publications > Reports > Informatics (CW) |
CW 296
S. Verbaeten
Termination analysis for abductive general logic programs
Abstract
We present an extension of the methods of Apt and Bezem for proving termination of general logic programs, to the case of abductive general logic programs. We consider programs executed under SLDNFA resolution, an abductive extension of SLDNF proposed by Denecker and De Schreye, w.r.t. an arbitrary safe selection rule. We show that the termination conditions for SLDNF of Apt and Bezem, namely acyclicity of the program and boundedness of the query, are not sufficient for ensuring termination under SLDNFA. A third syntactic condition, namely abductive nonrecursivity of the program and query, is proposed which prevents the abducing of an infinite number of abducible atoms. Acyclicity of the program, boundedness of the query and abductive nonrecursivity of the program and query form our sufficient termination condition for SLDNFA. By the best of our knowledge, this is the first work on termination of an abductive procedure for general logic programs.
report.pdf / mailto: S. Verbaeten