Search Images Maps Play YouTube News Gmail Drive More »
My library | Help | Advanced Book Search | Web History | Sign in

Books

Term Rewriting and All That

Front Cover
0 Reviews
Cambridge University Press, Aug 5, 1999 - Computers - 316 pages
This textbook offers a unified, self-contained introduction to the field of term rewriting. Baader and Nipkow cover all the basic material--abstract reduction systems, termination, confluence, completion, and combination problems--but also some important and closely connected subjects: universal algebra, unification theory, Gröbner bases, and Buchberger's algorithm. They present the main algorithms both informally and as programs in the functional language Standard ML (An appendix contains a quick and easy introduction to ML). Key chapters cover crucial algorithms such as unification and congruence closure in more depth and develop efficient Pascal programs. The book contains many examples and over 170 exercises. This is also an ideal reference book for professional researchers: results spread over many conference and journal articles are collected here in a unified notation, detailed proofs of almost all theorems are provided, and each chapter closes with a guide to the literature.
  

What people are saying - Write a review

We haven't found any reviews in the usual places.

Related books

Term Rewriting Systems
Term Rewriting Systems
Jan Willem Klop,Roel de Vrijer
Limited preview - 2003
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
Tobias Nipkow,Lawrence C. Paulson,Markus Wenzel
Limited preview - 2002
Handbook of Automated Reasoning
Handbook of Automated Reasoning, Volume 2
Alan J.A. Robinson,Andrei Voronkov
Limited preview - 2001
All related books »

Selected pages

Contents

II
1
III
7
IV
13
V
16
VI
18
VII
21
VIII
26
IX
28
XXXVI
160
XXXVII
164
XXXVIII
172
XXXIX
178
XL
182
XLI
184
XLII
187
XLIII
189

X
33
XI
34
XII
47
XIII
49
XV
58
XVI
59
XVII
61
XVIII
62
XIX
65
XX
71
XXI
73
XXII
79
XXIII
82
XXIV
91
XXV
93
XXVI
101
XXVII
104
XXVIII
111
XXIX
131
XXX
134
XXXI
135
XXXII
145
XXXIII
151
XXXIV
157
XXXV
158
XLIV
193
XLV
196
XLVI
198
XLVII
200
XLVIII
202
XLIX
207
L
211
LI
222
LII
223
LIII
224
LIV
230
LV
236
LVI
250
LVII
262
LVIII
265
LIX
267
LX
269
LXI
270
LXII
271
LXIII
273
LXIV
276
LXV
278
LXVI
284
LXVII
297
Copyright

Other editions - View all

Term Rewriting and All That
Term Rewriting and All That
Franz Baader,Tobias Nipkow
No preview available - 1998

Common terms and phrases

AC-unifier algebra algorithm alien subterms applied arbitrary assume binary function symbol Boolean Boolean rings Buchberger's algorithm C-unification coefficient collapsing computation confluent congruence closure contains critical pairs decidable decision procedure defined definition denote E-algebra elements equational theory equivalent example Exercise exists finite set free algebra function symbols functional programming ground terms halting problem hence holds homomorphism idempotent implementation implies induction infinite joinable Knuth-Bendix order left-linear Lemma lexicographic path order linear minimal complete set modulo monomial multiset nodes nontrivial normal form obtained occurs check orthogonal partial order proof prove recursive reduction order relation rewrite rule satisfies set of identities set of variables signature simplification order Sj-i solution step strict order substitution term rewriting system termination Theorem trivial Turing machine unary function undecidable unification problem unifier Var(t well-founded word problem yields

References to this book

From other books

Software Engineering with OBJ: Algebraic Specification in Action
Software Engineering with OBJ: Algebraic Specification in Action
Joseph A. Goguen,Grant Malcolm
No preview available - 2000
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
Tobias Nipkow,Lawrence C. Paulson,Markus Wenzel
Limited preview - 2002
All Book Search results »

From Google Scholar

E-a brainiac theorem prover
Stephan Schulz - 2002 - AI Communications
Theorem Proving Modulo
Gilles Dowek, Thérèse Hardin, Claude Kirchner - 2003 - Journal of Automated Reasoning
Combining superposition, sorts and splitting
Christoph Weidenbach - 2001
The rewriting calculus—Part I
HORATIU CIRSTEA, CLAUDE KIRCHNER - Logic Journal of IGPL
All Scholar search results »

References from web pages

Term rewriting and all that - Software, IEE Proceedings- [see also ...
and. all. that. by F. Baader and T. Nipkow. Cambridge University Press, 1998,301. +. xii pages,. ISBN. 0 521 45520 0, ...
ieeexplore.ieee.org/ iel4/ 5658/ 15162/ 00689298.pdf?arnumber=689298

Term Rewriting and All That by Franz Baader and Tobias Nipkow ...
Term Rewriting and All That by Franz Baader and Tobias Nipkow,. Cambridge University Press, 1998, ISBN 0-521-45520-0 (hardback), 301pp. ...
journals.cambridge.org/ production/ action/ cjoGetFulltext?fulltextid=72738

concurrency: llelism The Optimal Implementation of tmctional ...
Term Rewriting and All That. is written by Franz Baader. and Tobias Nipkow, and published by Cambridge University. Press, 1998 (paperback), 0-521-77920-0, ...
portal.acm.org/ citation.cfm?doid=505863.505888

Term Rewriting and All That
Term Rewriting and All That. Franz Baader and Tobias Nipkow. This is the first English language textbook offering a unified and self-contained introduction ...
www4.informatik.tu-muenchen.de/ ~nipkow/ TRaAT/

Term Rewriting
Term Rewriting and All That [Baader, Nipkow]. Table of contents:. Preface. 1 Motivating Examples. 2 Abstract Reduction Systems ...
tele.informatik.uni-freiburg.de/ Teaching/ ss02/ TR/ index.html

Confluence (term rewriting) - Wikipedia, the free encyclopedia
Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003; Term Rewriting and All That, Franz Baader and Tobias Nipkow, ...
en.wikipedia.org/ wiki/ Confluence_(term_rewriting)

Term rewriting system for code generation, and its termination ...
[Baader] Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, 1998. [Huang] Huang, ts: Two-Dimensional Signal Processing II: ...
okmij.org/ ftp/ Scheme/ PostL-paper.html

JSTOR: Term Rewriting Systems
The are two other recent English books on term rewriting: a textbook (F. Baader and T. Nipkow, Term rewriting and all that, Cambridge University Press, ...
links.jstor.org/ sici?sici=1079-8986(200406)10%3A2%3C223%3ATRS%3E2.0.CO%3B2-Q

Descendants and Origins in Term Rewriting (researchindex)
353 Term rewriting and all that (context) - Baader, Nipkow - 1998 ACM 259 Combinatory Logic (context) - Curry, Feys - 1958 ...
citeseer.ist.psu.edu/ bethke99descendants.html

Theory and Practice of Formal Proofs
27/11: Sections 3.1, 4.1-4.2, and 4.5-4.6 in Term Rewriting and All That . ... Term Rewriting and All That . Cambridge University Press, 1998. ...
www.diku.dk/ undervisning/ 2000e/ e00.202/

About the author (1999)

Franz Baader is a Professor in the Institute of Theoretical Computer Science at TU Dresden.

Bibliographic information

QR code for Term Rewriting and All That
TitleTerm Rewriting and All That
AuthorsFranz Baader, Tobias Nipkow
Editionillustrated
PublisherCambridge University Press, 1999
ISBN0521779200, 9780521779203
Length316 pages
Subjects ›  › 

Computers / Programming / Algorithms
Computers / Programming / General
Computers / Programming Languages / General
Computers / Reference
Computers / Software Development & Engineering / General
Mathematics / Discrete Mathematics
  
Export CitationBiBTeX EndNote RefMan