Title: Termination prediction for general logic programs
Authors: Shen, Yi-Dong
De Schreye, Danny
Voets, Dean
Issue Date: Mar-2009
Publisher: Department of Computer Science, K.U.Leuven
Series Title: CW Reports vol:CW536
Abstract: We present an approximation framework for attacking the undecidable termination problem of logic programs, as an alternative to current termination/non-termination proof approaches. We introduce an idea of termination prediction, which predicts termination of a logic program in case that neither a termination nor a non-termination proof is applicable. We establish a necessary and sufficient characterization of infinite (generalized) SLDNF-derivations with arbitrary (concrete or moded) queries, and develop an algorithm that predicts termination of general logic programs with arbitrary queries. We have implemented a termination prediction system and obtained quite satisfactory experimental results. Our prediction is 100% correct for all benchmark programs of the Termination Competition 2007, of which eighteen programs cannot be proved by the existing state-of-the-art analyzers like AProVE07, NTI, Polytool and TALP.
Publication status: published
KU Leuven publication type: IR
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
CW536.pdfDocument Published 349KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.