A Resolution Theorem for Algebraic Domains

1 Introduction

Domain Theory [Abramsky and Jung, 1994] is an abstract mathematical theory for programming semantics and has grown into a respected field on the borderline between math­ ematics and computer science. Studying relationships be­ tween domain theory and logic is of acknowledged impor­ tance in the field. There has been much work on the use of domain logics as logics of types and of program correctness, with a focus on functional and imperative languages. How­ ever, there has been only little work relating domain theory to logic programming or other AI paradigms, two exceptions be­ ing the application of methods from quantitative domain the­ ory to the semantic analysis of logic programming paradigms studied by Hitzler and Seda [Hitzler and Seda, 200x], and the work of Rounds and Zhang on the use of domain log­ ics for disjunctive logic programming and default reasoning [Rounds and Zhang, 2001].

The latter authors, in [Rounds and Zhang, 2001], intro­ duced a form of clausal logic generalized to coherent alge­ braic domains, motivated by investigating the logical content of the Smyth powerdomain construction. In the following, we study this clausal logic, henceforth called logic RZ for convenience. The occurrence of a proof theory based on a generalized resolution rule poses the question whether results underlying resolution-based logic programming systems can be carried over to the logic RZ. One of the most fundamen­ tal results underlying these systems is the resolution theorem which states that a clause X is a logical consequence of a the­ ory T if and only if it is possible to derive a contradiction, i.e. the empty clause, via resolution from the theory T U {-.X} [Robinson, 1965].

What we just called resolution theorem is certainly an im­ mediate consequence of the fact that resolution is sound and complete for classical logic. However, it is not obvious how it can be transfered to the logic RZ, mainly because it ne­ cessitates negating a clause, and negation is not available in the logic RZ in explicit form. This observation will lead our thoughts, and in the end we will develop conditions on the underlying domain which ensure that a negation is present which allows to prove an analogue of the theorem.

2 The Logic RZ

We assume that the reader is familiar with basic domain­ theoretic notions, and we will follow the terminology from [Abramsky and Jung, 1994] and [Rounds and Zhang, 2001]. In the following, (D, ~) will always be assumed to be a co­ herent algebraic cpo. We will also call these spaces domains. An element a E D is called an atom, or an atomic element, if whenever x ~ a we have x = a or x = l_. The set of all atoms of a domain is denoted by A( D).

Definition 2.1 Let D be a domain with set K(D) of compact elements. A clause is a finite subset ofK(D). If X is a clause and w E D, we write w f= X if there exists x E X with x ~ w. A theory is a set of clauses, which may be empty. An element w E D is a model of a theory T, written w f= T, if w f= X for all X E T . A clause X is called a logical consequence of a theory T, written T f= X, if w f= T implies w f= X. 1fT= {E}, then we write E f= X for {E} f= X. For two theories T and S, we say that T f= S ifT f= X for all X E S. We say that T and S are (logically) equivalent, written T rv S, if T f= S and S f= T . In order to avoid confusion, we will throughout denote the empty clause by{}, and the empty theory by 0. A theory T is (logically) closed if T f= X implies X E T for all clauses X. It is called consistent ifT ~ {}.

Rounds and Zhang originally set out to characterize logi­ cally the notion of Smyth powerdomain of coherent algebraic cpos. It naturally lead to the clausal logic RZ from Definition 2.1.

We can provide a sound and complete proof theory with simple rules. Consider the following rule, which we call sim­ plified hyperresolution.

Also consider the following rules, which we call the reduc­ tion rule and the extension rule.

Theorem 2.2 The system consisting of (shr). (ext) and (red) is complete.

For derivations with the rules from above, we use the sym­ bol f- as usual.

3 A Resolution Theorem

We simplify proof search via resolution by requiring stronger conditions on the domain.

Definition 3.1 An atomic domain is a coherent algebraic cpo D with the following property: For all c E K(D), the set A( c) ={pEA( D) I p ~ c} isfinite and c = UA(c).

We seek to represent a clause X by a finite set A(X) of atomic clauses which is logically equivalent to X . Given X= {a1 , . .. ,an}, wedefineA(X) = {{b1, ... , bn} I bi E A( ai ) for all i = 1, . . . , n} .

Theorem 3.2 For any clause X we have A( X) rv {X}.

In view of Theorem 3.2, it suffices to study T f- X for theories T and atomic clauses X. We can actually obtain a stronger result, as follows, which provides some kind of normal forms of derivations. For a theory T, define A(T) = {A(X) I X E T} .

Theorem 3.3 Let D be an atomic domain, T be a theory, X be a clause and

be a derivation. Then there exists a derivation

using only the atomic extension rule

and the multiple atomic shift rule (mas), as follows.

It also turns out that the rules from Theorem 3.3 are sound. We investigate next a notion of negation on domains.

Definition 3.4 An atomic domain is called an atomic do­ main with negation if there exists an involutive and Scott­ continuous negation function- : D ---> D with the properties:

• (i) - maps A( D) onto A( D).
• (ii) For all p, q E A(D) we have p Y q if and only if q = p.
• (iil) For every finite subset A<;;; A(D) such that pi qfor all p, q E A. the supremum U A exists.

Proposition 3.5 Let D be an atomic domain with negation. Thenforall c E K(D) wehavec = U{a I a E A(c)}.

The following result, an analogue to the resolution theo­ rem mentioned in the introduction, allows one to replace the search for derivations by search for contradiction.

Theorem 3.6 Let D be an atomic domain with negation. Let T be a theory and X be an atomic clause. Then T f= X if and only ifT U {{a} I a EX} f- {}.

On atomic domains with negation, we can therefore estab­ lish the following sound and complete proof principle.

Theorem 3. 7 LetT be a theory and X be a clause. Consider T' = A(T) . For every atomic clause A E A( X) attempt to show T' U {{a} I a E A} f- {} using (axt) and (mas) . If this succeeds, then T f= X. Conversely, if T f= X then there exists a derivation T' U {{a} I a E A} f- {}for each A E A(X) using only the above mentioned rules.

4 Conclusions

We have seen that for certain domains logical consequence in the logic RZ can be reduced to search for contradic­ tion, a result which yields a proof mechanism similar to that underlying the resolution principle used in resolution-based logic programming systems. The result should be understood as foundational for establishing logic programri1ing systems on hierarchical knowledge, built on a firm domain-theoretic background. Further research is being undertaken to substan­ tiate this.