Date of Award
1986
Degree Type
Dissertation
Degree Name
Doctor of Philosophy
Abstract
An obstacle to practical logic programming systems with equality is infinite computation. In the dissertation we study three strategies for eliminating infinite searches in Horn clause logic programming systems and develop an extension of Prolog that has the symmetry, transitivity and predicate substitutivity of equality built-in. The three strategies are: (1) Replacing logic programs with infinite search trees by equivalent logic programs with finite search trees; (2) Building into the inference machine the axioms that cause infinite search trees; (3) Detecting and failing searches of infinite branches.;The dissertation consists of two parts. General theories of the three strategies identified above are developed in Part I. In Part II we apply these strategies to the problem of eliminating infinite loops in logic programming with equality.;Part I. General Theories. We introduce the notion of CAS-equivalent logic programs: logic programs with identical correct answer substitutions. Fixpoint criteria for equivalent logic programs are suggested and their correctness is established. Semantic reduction is introduced as a means of establishing the soundness and completeness of extensions of SLD-resolution. The possibility of avoiding infinite searches by detecting infinite branches is explored. A class of SLD-derivations called repetitive SLD-derivation is distinguished. Many infinite derivations are instances of repetitive SLD-derivations. It is demonstrated that pruning repetitive SLD-derivations from SLD-trees does not cause incompleteness.;Part II. Extended Unification for Equality. An extension of SLD-resolution called SLDEU-resolution is presented. The symmetry, transitivity and predicate substitutivity of equality are built into SLDEU-resolution by extended unification. Extended unification, if unrestricted, also introduces infinite loops. We can eliminate some of these infinite loops by restricting SLDEU-resolution to non-repetitive right recursive SLDEU-resolution; this forbids extended unification of the first terms in equality subgoals and has a built-in mechanism for detecting repetitive derivations. The soundness and completeness of non-repetitive right recursive SLDEU-resolution are proved.
Recommended Citation
Chan, Kwok Hung, "Foundations Of Logic Programming With Equality" (1986). Digitized Theses. 1542.
https://ir.lib.uwo.ca/digitizedtheses/1542