An analysis of loop checking mechanisms for logic programs

DOI10.1016/0304-3975(91)90004-LMaRDI QIDQ1177923zbMATH OpenOpenAlexFDO

Authors Roland N. Bol, Krzysztof R. Apt, Jan Willem Klop

Publication date 26 June 1992

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(91)90004-l, https://ir.cwi.nl/pub/2010

zbMATH Keywords

infinite loops in computations of logic programsloop checks

Mathematics Subject Classification ID

Logic programming (68N17)

Review text

All methods of detecting divergence in computations of logic programs have been based on excluding some kinds of repetitions by so called loop checking. Loop checking mechanisms are systematically studied by considering their soundness, completeness and relative strength. It is shown that a natural concept of a simple loop check is too weak: no sound and complete loop checks exist even for programs with no function symbols. A number of sound simple loop checks is introduced and natural classes of Prolog programs without function symbols are identified for which the tests are complete. The loop checks are divided into three groups called equality checks, subsumption checks and context checks. The three groups of loop checks appear to be complete for programs with restricted recursion.

Recommendations

• Loop checks for logic programs with functions
• scientific article; zbMATH DE number 813263
• Redundancy elimination and loop checks for logic programs

Cites work

• A note on simplification orderings
• Contributions to the Theory of Logic Programming
• Controlling recursive inference
• Efficient loop detection in prolog using the tortoise-and-hare technique
• scientific article; zbMATH DE number 3872640 (Why is no real title available?)
• scientific article; zbMATH DE number 4199654 (Why is no real title available?)
• scientific article; zbMATH DE number 4057010 (Why is no real title available?)
• scientific article; zbMATH DE number 3731310 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• Partial evaluation in logic programming
• Recursive query processing: The power of logic
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture

Cited in

(22)

• Generalizing completeness results for loop checks in logic programming
• Loop checking in SLD-derivations by well-quasi-ordering of goals
• Abduction in logic programming: A new definition and an abductive procedure based on rewriting
• Redundancy elimination and loop checks for logic programs
• A framework for testing safety and effective computability
• Explanations as programs in probabilistic logic programming
• Deciding the bisimilarity relation between Datalog goals
• A non-termination criterion for binary constraint logic programs
• Termination prediction for general logic programs
• scientific article; zbMATH DE number 475191 (Why is no real title available?)
• scientific article; zbMATH DE number 549972 (Why is no real title available?)
• A metalogic programming approach: language, semantics and applications
• Two loop detection mechanisms: a comparison
• Knowledge base dynamics, abduction, and database updates
• scientific article; zbMATH DE number 813263 (Why is no real title available?)
• Detecting non-provable goals
• Loop checking in partial deduction
• A practical analysis of non-termination in large logic programs
• Termination Analysis of Logic Programs Based on Dependency Graphs
• Loop checks for logic programs with functions
• Non-termination in Term Rewriting and Logic Programming
• Enhancing global SLS-resolution with loop cutting and tabling mechanisms

This page was built for publication: An analysis of loop checking mechanisms for logic programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1177923)