Semantics of infinite tree logic programming

Abstract

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 suita..