@Incollection{Davis:HandbookAR:history:2001,
  title = {The Early History of Automated Deduction},
  author = {M. Davis},
  chapter = 1,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {I},
  pages = {3-15}}

@Incollection{BachmairGanzinger:HandbookAR:resolution:2001,
  title = {Resolution Theorem Proving},
  author = {L. Bachmair and H. Ganzinger},
  chapter = 2,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {I},
  pages = {19-99}}

@Incollection{Haehnle:HandbookAR:tableaux:2001,
  title = {Tableaux and Related Methods},
  author = {R. H\"ahnle},
  chapter = 3,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {I},
  pages = {100-178}}

@Incollection{DegtyarevVoronkov:HandbookAR:inverse:2001,
  title = {The Inverse Method},
  author = {A. Degtyarev and A. Voronkov},
  chapter = 4,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {I},
  pages = {179-272}}

@Incollection{Baaz+:HandbookAR:normal:2001,
  title = {Normal Form Transformations},
  author = {M. Baaz and U. Egly and A. Leitsch},
  chapter = 5,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {I},
  pages = {273-333}}

@Incollection{NonnengartWeidenbach:HandbookAR:small:2001,
  title = {Computing Small Clause Normal Forms},
  author = {A. Nonnengart and C. Weidenbach},
  chapter = 6,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {I},
  pages = {335-367}}

@Incollection{NieuwenhuisRubio:HandbookAR:paramodulation:2001,
  title = {Paramodulation-Based Theorem Proving},
  author = {R. Nieuwenhuis and A. Rubio},
  chapter = 7,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {I},
  pages = {371-443}}

@Incollection{BaaderSnyder:HandbookAR:unification:2001,
  title = {Unification Theory},
  author = {F. Baader and W. Snyder},
  chapter = 8,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {I},
  pages = {445-532}}

@Incollection{DershowitzPlaisted:HandbookAR:rewriting:2001,
  title = {Rewriting},
  author = {N. Dershowitz and D.A. Plaisted},
  chapter = 9,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {I},
  pages = {535-610}}

@Incollection{DegtyarevVoronkov:HandbookAR:sequent:2001,
  title = {Equality Reasoning in Sequent-Based Calculi},
  author = {A. Degtyarev and A. Voronkov},
  chapter = 10,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {I},
  pages = {611-706}}

@Incollection{ChouGao:HandbookAR:geometry:2001,
  title = {Automated Reasoning in Geometry},
  author = {S. C. Chou and X. S. Gao},
  chapter = 11,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {I},
  pages = {707-749}}

@Incollection{BockmayrWeispfenning:HandbookAR:numerical:2001,
  title = {Solving Numerical Constraints},
  author = {A. Bockmayr and V. Weispfenning},
  chapter = 12,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {I},
  pages = {751-842}}

@Incollection{Bundy:HandbookAR:induction:2001,
  title = {The Automation of Proof by Mathematical Induction},
  author = {A. Bundy},
  chapter = 13,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {I},
  pages = {845-911}}

@Incollection{Comon:HandbookAR:comon:2001,
  title = {Inductionless Induction},
  author = {H. Comon},
  chapter = 14,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {I},
  pages = {913-962}}

@Incollection{Andrews:HandbookAR:type:2001,
  title = {Classical Type Theory},
  author = {P.B. Andrews},
  chapter = 15,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {II},
  pages = {965-1007}}

@Incollection{Dowek:HandbookAR:higher:2001,
  title = {Higher-Order Unification and Matching},
  author = {G. Dowek},
  chapter = 16,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {II},
  pages = {1009-1062}}

@Incollection{Pfenning:HandbookAR:framework:2001,
  title = {Logical Frameworks},
  author = {F. Pfenning},
  chapter = 17,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {II},
  pages = {1063-1147}}

@Incollection{BarendregtGeuvers:HandbookAR:assistant:2001,
  title = {Proof-Assistants Using Dependent Type Systems},
  author = {H. Barendregt and H. Geuvers},
  chapter = 18,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {II},
  pages = {1149-1238}}

@Incollection{Dix+:HandbookAR:nmr:2001,
  title = {Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations},
  author = {J. Dix and U. Furbach and I. Niemel{\"a}},
  chapter = 19,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {II},
  pages = {1241-1354}}

@Incollection{Baaz+:HandbookAR:manyvalued:2001,
  title = {Automated Deduction for Many-Valued Logics},
  author = {M. Baaz and C.G. Ferm{\"u}ller and G. Salzer},
  chapter = 20,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {II},
  pages = {1355-1402}}

@Incollection{Ohlbach+:HandbookAR:encoding:2001,
  title = {Encoding Two-Valued Nonclassical Logics in Classical Logic},
  author = {H.J. Ohlbach and A. Nonnengart and M.\ de Rijke and D.\ Gabbay},
  chapter = 21,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {II},
  pages = {1403-1486}}

@Incollection{Waaler:HandbookAR:nonclassical:2001,
  title = {Connections in Nonclassical Logics},
  author = {A. Waaler},
  chapter = 22,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {II},
  pages = {1487-1578}}

@Incollection{Calvanese+:HandbookAR:dl:2001,
  title = {Reasoning in Expressive Description Logics},
  author = {D. Calvanese and G. De Giacomo and M. Lenzerini and D. Nardi},
  chapter = 23,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {II},
  pages = {1581-1634}}

@Incollection{ClarkeSchlingloff:HandbookAR:checking:2001,
  title = {Model Checking},
  author = {E.M. Clarke and H. Schlingloff},
  chapter = 24,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {II},
  pages = {1635-1790}}

@Incollection{Fermuller+:HandbookAR:decision:2001,
  title = {Resolution Decision Procedures},
  author = {C.~Ferm{\"u}ller and A. Leitsch and U. Hustadt and T. Tammet},
  chapter = 25,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {II},
  pages = {1791-1849}}

@Incollection{Ramakrishnan+:HandbookAR:term:2001,
  title = {Term Indexing},
  author = {I.V. Ramakrishnan and R. Sekar and A. Voronkov},
  chapter = 26,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {II},
  pages = {1853-1964}}

@Incollection{Weidenbach:HandbookAR:spass:2001,
  title = {Combining Superposition, Sorts and Splitting},
  author = {C. Weidenbach},
  chapter = 27,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {II},
  pages = {1965-2013}}

@Incollection{LetzStenz:HandbookAR:me:2001,
  title = {Model Elimination and Connection Tableau Procedures},
  author = {R. Letz and G. Stenz},
  chapter = 28,
  booktitle = {Handbook of Automated Reasoning},
  publisher = {Elsevier Science},
  editor = {A. Robinson and A. Voronkov},
  year = 2001,
  volume = {II},
  pages = {2015-2114}}