Resolution in the Smyth powerdomain
Guo‐Qiang Zhang, William C. Rounds · Electronic Notes in Theoretical Computer Science · 1997
The purposes of this paper are (i) to give a new, efficient representation of Smyth powerdomains as 0-inhabited information systems, following the style of Scott; (ii) to introduce, as a consequence of this representation, a generalized resolution method for an arbitrary Smyth powerdomain and show the soundness and completeness of this method. The connection of (i) with (ii) comes from the observation that the elements of a Smyth powerdomain are semantically equivalent to the basic notion of "clauses' as used in the area of logic programming.