SUPREMA OF OPEN AND CLOSED FORMULAS AND THEIR APPLICATION TO RESOLUTION

We discuss an algebra of open formulas, SOAF. The algebra is equipped with the operator mgi-o, which computes suprema of sets of open formul as, ordered according to a weak form of instance ordering. Rules to co mpute such points are provided. These rules supply a computation proce dure to unify open formulas. Next, we consider an algebra of closed fo rmulas, SCAF. It has an operator mgi-c, which computes suprema of set of formulas ordered according to the instance preordering. We give rul es to compute such points. These rules supply a computation procedure to unify closed formulas. Relations between these operators and unific ation in open and closed formulas, and weak unification in closed form ulas, are addressed. Also, we consider clausal formulas and apply thes e considerations to the resolution process. This provides a rule alter native to resolution and shows that resolvents can be expressed and ef fectively obtained as suprema of closed formulas. The new rule need no t resort to renaming, unification. and instantiation as first class op erations. Finally, applications to resolution in Horn clause logic and logic programming are discussed. This leads to a more compact theory of logic programming, in which, for instance, the domain of substituti ons is eliminated. (C) 1995 Academic Press. Inc.