Semantics of infinite tree logic programming

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 T P 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 T P, exactly correspond to the operational semantics. The corresponding proofs in the case where no unequations are considered are relatively straightforward mainly because the function T P 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 T P; 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 T P and the concept of completed logic programs and negation-as-failure.

Authors

• Joxan Jaffar Andrew E. Santosa
• Peter J. Stuckey Monash University

Keywords

No keywords are indexed for this paper.