Handbook of Automated Reasoning, volunteer readers

We need additional second readers for the Handbook of Automated Reasoning,
to be published in two volumes this year by Elsevier Science and MIT

The table of contents is enclosed. If you volunteer to referee one or
more chapters please contact Andrei Voronkov at voronkov@csd.uu.se.

The second readers are expected to read the chapter(s) thoroughly and
check the formal content carefully.

The chapters should treat the corresponding topics as completely as
possible, therefore the readers should in particular comment on this.

Names of second readers will appear in the Handbook on the bottom of
the facing page of the corresponding chapter.

We will appreciate it very much if you will help us in putting together
a volume of high quality.

Best regards,
Alan Robinson,
Andrei Voronkov


1. If you are puzzled by the term "second reader", here is an
explanation. The term "referee" is inappropriate when all articles
are invited. The authors are considered to be the first readers of
their chapters.

2. When selecting a chapter to referee please take into attention
the size of the article and think whether you can read it through in
1-2 months. The page format is essentially the same as in the Handbook
of Theoretical Computer Science.


Handbook of Automated Reasoning

edited by Alan Robinson and Andrei Voronkov

Table of contents

Resolution decision procedures, 43 pages
  Alexander Leitsch,
  Christian Fermüller,
  Tanel Tammet

A theory of resolution, 65 pages
  Leo Bachmair,
  Harald Ganzinger

Higher order unification and matching, 51 pages
  Gilles Dowek

Automated reasoning in geometry, 43 pages
  Xiao-Shan Gao,
  Shang-Ching Chou

The early history of automated deduction, 13 pages
  Martin Davis

The automation of proof by mathematical induction, 66 pages
  Alan Bundy

Normal form transformations, 36 pages
  Matthias Baaz,
  Uwe Egly,
  Alexander Leitsch

Reasoning in expressive description logics, 59 pages
  Diego Calvanese,
  Giuseppe De Giacomo,
  Maurizio Lenzerini,
  Daniele Nardi

Proof-assistants using type theory, 43 pages
  Henk Barendregt,
  Herman Geuvers

Nonmonotonic reasoning: towards efficient calculi and implementation, 113 pages
  Jurgen Dix,
  Ulrich Furbach,
  Ilkka Niemelä

Unification theory, 85 pages
  Franz Baader,
  Wayne Snyder

Equality reasoning in sequent-based calculi, 94 pages
  Anatoli Degtyarev,
  Andrei Voronkov

Classical type theory, 43 pages
  Peter Andrews

Model checking, 122 pages
  Edmund Clarke,
  Holger Schlingloff

Paramodulation-based theorem proving, 55 pages
  Robert Niewenhuis,
  Alberto Rubio

Inductionless induction, 47 pages
  Hubert Comon

Model elimination and connection procedures, 72 pages
  Reinhold Letz,
  Gernot Stenz

Term indexing, 115 pages
  Andrei Voronkov

Tableaux and connections, 67 pages
  Reiner Hähnle

On generating small clause normal forms, 33 pages
  Andreas Nonnengart,
  Christoph Weidenbach

Encoding non-classical logics in classical logic, 58 pages
  Dov Gabbay,
  Andreas Nonnengart,
  Hans-Jürgen Ohlbach

A tutorial on logical frameworks, 89 pages
  Frank Pfenning

Automated deduction for many-valued logics, 47 pages
  Matthias Baaz,
  Christian Fermüller,
  Gernot Salzer

The inverse method, 56 pages
  Anatoli Degtyarev,
  Grigory Mints,
  Tanel Tammet,
  Andrei Voronkov

Rewriting, 62 pages
  Nachum Dershowitz

Solving numerical constraints, 70 pages
  Alexander Bockmayr,
  Volker Weispfenning

Tableaux and connections for non-classical logics, 59 pages
  Arild Waaler,
  Lincoln Wallen

Combining superposition, sorts and splitting, 40 pages
  Christoph Weidenbach