Practical Methods for Proving Termination of General Logic Programs

TL;DR

This paper presents a methodology for proving the termination of general logic programs with negation under the Prolog selection rule, facilitating formalization in non-monotonic reasoning.

Contribution

It introduces new notions like low-, weakly up-, and up-acceptable programs to systematically prove termination of logic programs with negation.

Findings

The methodology effectively distinguishes parts of programs based on termination dependence.

It formalizes interesting non-monotonic reasoning problems using terminating logic programs.

The approach is applicable to programs with negation under the Prolog selection rule.

Abstract

Termination of logic programs with negated body atoms (here called general logic programs) is an important topic. One reason is that many 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 w.r.t. the Prolog selection rule. The idea is to distinguish parts of the program depending on whether or not their termination depends on the selection rule. To this end, the notions of low-, weakly up-, and up-acceptable program are introduced. We use these notions to develop a methodology for proving termination of general logic programs, and show how interesting problems in non-monotonic reasoning can be formalized and implemented by means of terminating general logic programs.