We address the problem of declarative and operational semantics for logic programming in the domain of infinite trees. We consider logic programming semantics based on the now familiar function TP which maps from and into interpretations of the program P. The main point of departure of our work from the literature is that we include unequations in our treatment. Specifically, we prove that the intuitive notions of success and finite failure, defined in terms of TP, exactly correspond to the operational semantics. The corresponding proofs in the case where no unequations are considered are relatively straightforward mainly because the function TP has a closure property with respect to a suitable metric space of infinite trees. When unequations are considered, however, the function loses this property and consequently the proofs become more complex. The key to our treatment is a result about images of TP; we show that these sets have a property analogous to closure. Finally, we also prove certain results pertaining to infinite derivations. These concern the greatest fixpoint of TP and the concept of completed logic programs and negation-as-failure. © 1986.
Jaffar, J., & Stuckey, P. J. (1986). Semantics of infinite tree logic programming. Theoretical Computer Science, 46(C), 141–158. https://doi.org/10.1016/0304-3975(86)90027-7