Generalizing completeness results for loop checks in logic programming

DOI10.1016/0304-3975(92)90164-BMaRDI QIDQ1199926zbMATH OpenFDO

Authors Roland N. Bol

Publication date 17 January 1993

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

Full work available at URL https://doi.org/10.1016/0304-3975(92)90164-B

zbMATH Keywords

Loop checkingnormal SLD derivations

Mathematics Subject Classification ID

Logic programming (68N17)

Review text

Loop checking is one of the fundamental problems encountered during the search of effective algorithms for logic programming. This complex problem cannot be solved in full generality (even in absence of function symbols). In \textit{R. N. Bol, K. R. Apt} and \textit{J. W. Klop} [ Theor. Comput. Sci. 86, No. 1, 35-79 (1991; Zbl 0741.68027)], (sound) loop checks were introduced and there were determined subclasses of programs for which these checks are complete. The Generalization Theorem of the present paper presents a method to extend these subclasses under certain natural conditions. A crucial role in this approach plays the notion of nonrecursive extension of a logic program. The proof itself calls attention to normal SLD derivations which put extra requirements on the used most general unifiers (limiting needless renaming of variables in a derivation).

Recommendations

• scientific article; zbMATH DE number 813263
• scientific article; zbMATH DE number 549972
• An analysis of loop checking mechanisms for logic programs
• Redundancy elimination and loop checks for logic programs
• Loop checks for logic programs with functions

Cites work

• An analysis of loop checking mechanisms for logic programs
• An Efficient Unification Algorithm
• 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 3982556 (Why is no real title available?)
• scientific article; zbMATH DE number 4057010 (Why is no real title available?)
• scientific article; zbMATH DE number 408774 (Why is no real title available?)
• scientific article; zbMATH DE number 549972 (Why is no real title available?)
• scientific article; zbMATH DE number 1142320 (Why is no real title available?)
• Partial evaluation in logic programming
• Recursive query processing: The power of logic

Cited in

(7)

• The role of standardising apart in logic programming
• Loop checking in SLD-derivations by well-quasi-ordering of goals
• Redundancy elimination and loop checks for logic programs
• Completeness and counter-example generations of a basic protocol logic (extended abstract)
• scientific article; zbMATH DE number 549972 (Why is no real title available?)
• scientific article; zbMATH DE number 813263 (Why is no real title available?)
• Loop checks for logic programs with functions

This page was built for publication: Generalizing completeness results for loop checks in logic programming

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