2005/12/14 by Yi-Dong Shen, Shen, Yi-Dong, Danny De Schreye +1
Computer Science · #D.1.6 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Programming Languages (cs.PL) #Software Testing and Debugging Techniques #cs.LO #cs.PL
paper · pdf · doi:10.48550/arxiv.cs/0512055
24 Pages
arxiv created 2005/12/14 · openalex publication_date 2005/12/14 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The termination problem of a logic program can be addressed in either a static or a dynamic way. A static approach performs termination analysis at compile time, while a dynamic approach characterizes and tests termination of a logic program by applying a loop checking technique. In this paper, we present a novel dynamic approach to termination analysis for general logic programs with moded queries. We address several interesting questions, including how to formulate an SLDNF-derivation for a moded query, how to characterize an infinite SLDNF-derivation with a moded query, and how to apply a loop checking mechanism to cut infinite SLDNF-derivations for the purpose of termination analysis. The proposed approach is very powerful and useful. It can be used (1) to test if a logic program terminates for a given concrete or moded query, (2) to test if a logic program terminates for all concrete or moded queries, and (3) to find all (most general) concrete/moded queries that are most likely terminating (or non-terminating).