Skip to main content
main-content

Über dieses Buch

In this monograph we study two generalizations of standard unification, E-unification and higher-order unification, using an abstract approach orig­ inated by Herbrand and developed in the case of standard first-order unifi­ cation by Martelli and Montanari. The formalism presents the unification computation as a set of non-deterministic transformation rules for con­ verting a set of equations to be unified into an explicit representation of a unifier (if such exists). This provides an abstract and mathematically elegant means of analysing the properties of unification in various settings by providing a clean separation of the logical issues from the specification of procedural information, and amounts to a set of 'inference rules' for unification, hence the title of this book. We derive the set of transformations for general E-unification and higher­ order unification from an analysis of the sense in which terms are 'the same' after application of a unifying substitution. In both cases, this results in a simple extension of the set of basic transformations given by Herbrand­ Martelli-Montanari for standard unification, and shows clearly the basic relationships of the fundamental operations necessary in each case, and thus the underlying structure of the most important classes of term unifi­ cation problems.

Inhaltsverzeichnis

Frontmatter

Chapter 1. Introduction

Abstract
Most researchers consider the modern period of automated logic to have begun with the discovery of resolution by J.A. Robinson in 1963 at the Argonne National Laboratory. Previously, it was known by the Herbrand-Skolem-Godel theorem that semi-decision procedures could be designed for first-order logic by reducing the question of the unsatisfiability of a set of first-order formulae to the question of unsatisfiability of (roughly) a set of certain ground formulae derived from the original set in an effective way (for example, see [32]). But until Robinson invented the simple and powerful inference rule known as resolution [139], no practically efficient semi-decision procedure had been found. The crucial component of this seminal discovery was in fact the rediscovery by Robinson of the process of unification, which had been discovered by Herbrand in his thesis 33 years earlier (see Appendix 3).1
Wayne Snyder

Chapter 2. Preview

Abstract
The method of transformations for solving unification problems is much like the well-known method used for solving systems of linear equations known as Gaussian elimination. In Gaussian elimination, the original system of equations is transformed step by step (by variable elimination) into a solved system, that is, a system whose solution is obvious. Similarly, a unification problem is a set {u1v1,..., u n v n } of equations between terms (sometimes called a disagreement set) to be (jointly) unified. (We consider these equations to be unoriented.) The method of transformations consists of applying simple transformations, some akin to variable elimination, until a “solved” system S′ is obtained whose solution is obvious (in a sense to be made precise below).
Wayne Snyder

Chapter 3. Preliminaries

Abstract
This section contains an outline of the major definitions and results related to unification and equational logic, and is basically consistent with [77] and [49]. A separate section of preliminaries relating to higher-order unification will be given in Chapter §7.
Wayne Snyder

Chapter 4. E-Unification

Abstract
In Section §3.3 we defined the standard unification of terms, most general unifiers, and showed how the abstract non-deterministic method of transformations on systems of equations provides a procedure for unification which either fails or terminates with an explicit representation of the mgu of the original system. The notion of standard unification is based on making two (first-order) terms syntactically identical, but in fact, we could generalize this to any relation P on terms, defining “P-unification” to be the problem of determining for two terms u and v if there exists some substitution θ such that (θ(u),θ(v))∊ P. In this section we present the basic notions of E-unification, where this relation P is represented by a finite set of equations E. The two following chapters will present a general procedure for E-unification via the method of transformations; later in this monograph, in Chapter §7, we present a generalization of unification to higher-order terms, and develop a non-deterministic procedure in the same fashion.
Wayne Snyder

Chapter 5. E-Unification via Transformations

Abstract
We now show how to extend the set of transformations ST given in Section §3.3 to perform E-unification of a system under some arbitrary E, and develop the non-deterministic completeness of the method using a new formalism for ‘proofs’ that two terms are E-unifiable, known as equational proof trees. The new set of transformations is fully general in that it is capable of enumerating a CSU E (S) for any system S and set of equations E, and we intend this chapter to provide a paradigm for the abstract study of complete methods for general E-unification. The set of E-unifiers found by this method is highly redundant, however, and in the next chapter, we show how to restrict this method to avoid rewriting at variable occurrences while still retaining the ability to enumerate a CSU E (S).
Wayne Snyder

Chapter 6. An Improved Set of Transformations

Abstract
In the last chapter we presented a set of transformations BT complete for arbitrary equational theories E, but which were prohibitively inefficient. In this chapter we present a restricted version of BT, called T, which solves these problems, and prove its completeness.
Wayne Snyder

Chapter 7. Higher Order Unification

Abstract
Higher-order unification is a method for unifying terms in the Simple Theory of Types [28], that is, given two typed lambda-terms e1 and e2, finding a substitution σ for the free variables of the two terms such that σ(e1) and σ(e2) are equivalent under the conversion rules of the calculus. As discussed above, this problem is fundamental to theorem proving in higher-order contexts (see Chapter §1 for references). In this chapter, we adapt the method of transformations to higher-order unification.
Wayne Snyder

Chapter 8. Conclusion

Abstract
In this monograph we studied general E-unification and higher-order unification using the method of non-deterministic transformations on systems of equations originated by Herbrand and developed in the case of standard first-order unification by Martelli and Montanari. This formalism provides an abstract and mathematically elegant means of analysing the properties of these more complex types of unification problems by providing a clean separation of the logical issues from the specification of procedural information.In each case, we extended the basic set of transformations ST for standard unification by analysing the precise manner in which terms are defined to be ’the same’ in these two generalizations of unification, i.e., modulo the least congruence induced by the set of equations for E-unification,and modulo the conversion rules of the typed lambda calculus for higher-order unification.
Wayne Snyder

Backmatter

Weitere Informationen