Semantics of Logic Programs and Representation of Smyth Powerdomain

Abstract

This paper provides a representation of the Smyth powerdomain in order to base the semantics of logic programs on Scott’s information systems. A new notion of ideal elements, called disjunctive states, is introduced. Disjunctive states are built from clauses over the token set of the underlying information system to capture disjunctive information. They are closed under Robinson’s hyperresolution rule. We establish an order-isomorphism between disjunctive states and compact, saturated sets, for which injectivity and surjectivity correspond to the soundness and completeness of hyperresolution. A key step for the order-isomorphism is the Hoffman-Mislove Theorem in light of a lemma by Keimel and Paseka. As an application, we provide a couple of specific Smyth powerdomain examples suitable for logic programming. In general, the notion of disjunctive state is applicable to sequent structures, or nondeterministic information systems. We show that the hyperresolution rule is sound and complete for sequent structures as well, making it possible to interpret a disjunctive logic program directly as a sequent structure.