Skip to main content
SpringerLink
Log in
Birkhäuser

A Proof Theory for General Unification

  • Book
  • © 1991

Overview

Authors:
  1. Wayne Snyder

    1. Department of Computer Science, Boston University, Boston, USA

    View author publications

    You can also search for this author in PubMed   Google Scholar

Part of the book series: Progress in Computer Science and Applied Logic (PCS, volume 11)

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book USD 54.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (8 chapters)

  1. Front Matter

    Pages i-vii
    Download chapter PDF

  2. Introduction

    • Wayne Snyder
    Pages 1-6

  3. Preview

    • Wayne Snyder
    Pages 7-16

  4. Preliminaries

    • Wayne Snyder
    Pages 17-48

  5. E-Unification

    • Wayne Snyder
    Pages 49-60

  6. E-Unification via Transformations

    • Wayne Snyder
    Pages 61-82

  7. An Improved Set of Transformations

    • Wayne Snyder
    Pages 83-122

  8. Higher Order Unification

    • Wayne Snyder
    Pages 123-153

  9. Conclusion

    • Wayne Snyder
    Pages 154-155

  10. Back Matter

    Pages 157-178
    Download chapter PDF
Back to top

Keywords

About this book

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.

Authors and Affiliations

  • Department of Computer Science, Boston University, Boston, USA

    Wayne Snyder

Bibliographic Information

  • Book Title: A Proof Theory for General Unification

  • Authors: Wayne Snyder

  • Series Title: Progress in Computer Science and Applied Logic

  • DOI: https://doi.org/10.1007/978-1-4612-0435-0

  • Publisher: Birkhäuser Boston, MA

  • eBook Packages: Springer Book Archive

  • Copyright Information: Springer Science+Business Media New York 1991

  • Hardcover ISBN: 978-0-8176-3593-0Published: 01 November 1991

  • Softcover ISBN: 978-1-4612-6758-4Published: 30 September 2012

  • eBook ISBN: 978-1-4612-0435-0Published: 06 December 2012

  • Series ISSN: 2297-0576

  • Series E-ISSN: 2297-0584

  • Edition Number: 1

  • Number of Pages: VII, 178

  • Topics: Theory of Computation, Mathematical Logic and Foundations

Publish with us

Policies and ethics

Back to top

Search

Navigation