A Proof Theory for General Unification
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 Montana
- PDF / 14,728,292 Bytes
- 181 Pages / 439 x 666 pts Page_size
- 19 Downloads / 246 Views
Progress in Computer Science and Applied Logic Volume 11
Editor John C. Cherniavsky, Georgetown University
Associate Editors Robert Constable, Cornell University Jean Gallier, University of Pennsylvania Richard Platek, Cornell University Richard Statman, Carnegie-Mellon University
Wayne Snyder
A Proof Theory for General Unification
Springer-Science+Business Media, LLC
Wayne Snyder Departtnent of Computer Seience Boston University Boston, MA 02215
Library ofCongress Cataloging-in-Publication Data Snyder, Wayne, 1955A proof theory for general unification / by Wayne Snyder. p. cm. -- (Progress in computer science and applied logic v. 11) Includes bibliographical references. ISBN 978-1-4612-6758-4 ISBN 978-1-4612-0435-0 (eBook) DOI 10.1007/978-1-4612-0435-0
(hard : acid-free) 1. Automatie theorem proving.
I. Title.
QA76.9.A96S6 511.3--dc20
II. Series. 91-28685 CIP
Printed on acid-free paper.
© Springer Science+Business Media New York 1991 Originally published by Birkhäuser Boston in 1991 Softcover reprint ofthe hardcover 1st edition 1991 All rights reserved. No part of this publication may be reproduced, stored in a retrieval system,or transmitted, in any form or by any means, electronic. mechanical, photocopying. recording, or otherwise. without prior permission of the copyright owner. Permission to photocopy for internal or personal use of specific clients is granted by Springer-Science+Business Media, LLC for libraries and other users registered with the Copyright Clearance Center (CCC), provided that the base fee of $0.00 per copy, plus $0.20 per page is paid directly to CCC, 21 Congress Street, Salem, MA 01970, U.S.A. Special requests should be addressed directly to Springer-Science+Business Media, LLC.
ISBN 978-1-4612-6758-4 Camera ready text prepared by the author in LaTeX.
987654321
Table of Contents
Preface
Vll
Chapter 1: Introduction
1
Chapter 2: Preview.
7
.
Chapter 3: Preliminaries
3.1 3.2 3.3 3.4 3.5
Algebraic Background Substitutions.... Unification by Transformations on Systems Equational Logic . . . . . Term Rewriting. . . . . . 3.5.1 Termination Orderings Confluence...... 3.5.2 3.6 Completion of Equational Theories
Chapter 4: E- Unification
4.1 4.2
Basic Definitions and Results Methods for E- Unification .
Chapter 5: E- Unification via Transformations
5.1 5.2 5.3
The Set of Transformations BT Soundness of the Set BT . . Completeness of the Set BT
Chapter 6: An Improved Set of Transformations
6.1 6.2 6.3 6.4 6.5 6.6 6.7 6.8 6.9
Ground Church-Rosser Systems. Completeness of the Set T . . . . . Surreduction........... Completeness of the Set T Revisited Relaxed Paramodulation . . Previous Work . . . . . . Eager Variable Elimination. Current and Future Work Conclusion........
17 17 20 23
28 33
34 37
44 49
49 52
61 61
65 67 83
83
93 104
109 112 116 119
120 122
VI
CONTENTS
Chapter 7: Higher Order Unification . . . . . 7.1 Preliminaries............... 7.2 Higher Order Unification via Transformations 7.2.1 Transformations for Higher Order Unification 7.2.2
Data Loading...
