The book represents an attempt by the authors to gather together the most fundamental results on string-rewriting systems. The goal is to explain these results in such a way that they can be understood and used in studies relating to more general rewriting, automated deduction, and algorithmic problems of algebraic structures. The authors have concentrated on presenting basic material that ought to be a prerequisite for understanding more specialized material. The monograph opens with the preliminaries of string-rewriting systems followed by length as the basis for reduction. Monadic string-rewriting systems is covered as well as length-reducing non-monadic string-writing systems. The book closes with the subjects of algebraic protocols and algebraic properties. When the reader has mastered the material in the core of the book (Chapters 1-4), then that person should be equipped to explore the ever-growing body of literature in the field of string-rewriting systems. Both authors have been active in the field of string-rewriting systems and have lectured on the subject in several universities. Lecture notes have been produced and distributed. This monograph is a result of revising and rewriting those notes. This monograph is written for independent study by researchers in theoretical computer science or in the foundation of artificial intelligence. This book is not intended as a textbook, but it certainly could be used as a textbook in computer science. It could be used for a course entitled "Rewriting Systems," or "String Rewriting," or "Foundations of Artificial Intelligence."
Author(s): Ronald V. Book, Friedrich Otto
Series: Texts and Monographs in Computer Science
Publisher: Springer
Year: 1993
Language: English
Pages: 195
Cover ......Page 1
Preface ......Page 3
Contents ......Page 5
0.1 Historical Development ......Page 7
0.2 An Outline of Recent Developments ......Page 9
0.3 Contents of the Monograph ......Page 12
1.1 Abstract Reduction Systems ......Page 15
1.2 Reduction Modulo an Equivalence Relation ......Page 21
1.3 Strings, Languages and Automata ......Page 28
1.4 Some Turing Machine Constructions ......Page 33
1.5 Bibliographic Remarks ......Page 40
2.1 Rewriting Systems for Strings ......Page 41
2.2 Computing Normal Forms ......Page 47
2.3 Testing for Local Confluence ......Page 56
2.4 The Knuth-Bendix Completion Procedure ......Page 58
2.5 Some Undecidable Properties ......Page 63
2.6 Bibliographic Remarks ......Page 69
3.1 Basic Properties ......Page 71
3.2 Testing for Confluence ......Page 74
3.3 Confluence on a Single Class ......Page 76
3.4 Equivalent Systems ......Page 77
3.5 Church-Rosser Congruences ......Page 83
3.6 Other Systems Based on Length ......Page 86
3.7 Bibliographic Remarks ......Page 94
4.1 Basic Properties ......Page 97
4.2 Specification of Formal Languages ......Page 100
4.3 A Decision Procedure ......Page 104
4.4 Applications of the Decision Procedure ......Page 110
4.5 Limitations of the Decision Procedure ......Page 112
4.6 Bibliographic Remarks ......Page 116
5.1 Presenting Recursively Enumerable Languages ......Page 119
5.2 Some Undecidability Results ......Page 125
5.3 Some Questions on Congruential Languages ......Page 134
5.4 Bibliographic Remarks ......Page 136
6.1 Basic Properties ......Page 137
6.2 Security and Cascade Protocols ......Page 143
6.3 Security and Name-Stamp Protocols ......Page 149
6.4 Bibliographic Remarks ......Page 152
7.1 Finite Monoid-Presentations ......Page 153
7.2 Tietze Transformations ......Page 159
7.3 Some Undecidability Results ......Page 163
7.4 The Free Monoid Problem ......Page 168
7.5 The Group Problem ......Page 174
7.6 Bibliographic Remarks ......Page 176
References ......Page 181
Index ......Page 190