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

Original language | English |
---|---|

Pages (from-to) | 141-158 |

Number of pages | 18 |

Journal | Theoretical Computer Science |

Volume | 46 |

Issue number | C |

DOIs | |

Publication status | Published - 1 Jan 1986 |