A methodology for proving termination of general logic programs

Termination of logic programs with negated body atoms, here called general logic programs, is an important topic. This is also due to the fact that the computational mechanisms used to process negated atoms, like Clark's negation as failure and Chan's constructive negation, are based on termination conditions. This paper introduces a methodology for proving termination of general logic programs, when the Prolog selection rule is considered. This methodology is based on the notions of low-up-acceptable program. We prove that low-up-acceptable programs characterize a class of general logic programs which terminate for a large class of queries, which contains the set of all ground queries. We consider as operational model SLD-resolution augmented with a procedure to deal with negative literals, known as Chan's constructive negation. General logic programs can be used to express concepts and problems in non-monotonic reasoning. We show here, that interesting problems in non-monotonic reasoning can be formalized and implemented by means of up-low-general logic programs.