Automated Termination Proofs for Logic Programs by Term Rewriting

Details Automated Termination Proofs for Logic Programs by Term Rewriting Automated Termination Proofs for Logic Programs by Term Rewriting

2008-03-02

arxiv.org/abs/0803.0014v2

Computer Science

Logic in Computer Science

49 pages

Scientific paper

There are two kinds of approaches for termination analysis of logic programs: "transformational" and "direct" ones. Direct approaches prove termination directly on the basis of the logic program. Transformational approaches transform a logic program into a term rewrite system (TRS) and then analyze termination of the resulting TRS instead. Thus, transformational approaches make all methods previously developed for TRSs available for logic programs as well. However, the applicability of most existing transformations is quite restricted, as they can only be used for certain subclasses of logic programs. (Most of them are restricted to well-moded programs.) In this paper we improve these transformations such that they become applicable for any definite logic program. To simulate the behavior of logic programs by TRSs, we slightly modify the notion of rewriting by permitting infinite terms. We show that our transformation results in TRSs which are indeed suitable for automated termination analysis. In contrast to most other methods for termination of logic programs, our technique is also sound for logic programming without occur check, which is typically used in practice. We implemented our approach in the termination prover AProVE and successfully evaluated it on a large collection of examples.

Affiliated with

Also associated with

No associations

Rating

Automated Termination Proofs for Logic Programs by Term Rewriting does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Automated Termination Proofs for Logic Programs by Term Rewriting, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Automated Termination Proofs for Logic Programs by Term Rewriting will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-359482