Abstract is missing.
- Preface
- The Early History of Automated DeductionMartin Davis. 3-15
- Resolution Theorem ProvingLeo Bachmair, Harald Ganzinger. 19-99
- Tableaux and Related MethodsReiner Hähnle. 100-178
- The Inverse MethodAnatoli Degtyarev, Andrei Voronkov. 179-272
- Normal Form TransformationsMatthias Baaz, Uwe Egly, Alexander Leitsch. 273-333
- Computing Small Clause Normal FormsAndreas Nonnengart, Christoph Weidenbach. 335-367
- Paramodulation-Based Theorem ProvingRobert Nieuwenhuis, Albert Rubio. 371-443
- Unification TheoryFranz Baader, Wayne Snyder. 445-532
- RewritingNachum Dershowitz, David A. Plaisted. 535-610
- Equality Reasoning in Sequent-Based CalculiAnatoli Degtyarev, Andrei Voronkov. 611-706
- Automated Reasoning in GeometryShang-Ching Chou, Xiao-Shan Gao. 707-749
- Solving Numerical ConstraintsAlexander Bockmayr, Volker Weispfenning. 751-842
- The Automation of Proof by Mathematical InductionAlan Bundy. 845-911
- Inductionless InductionHubert Comon. 913-962
- Classical Type TheoryPeter B. Andrews. 965-1007
- Higher-Order Unification and MatchingGilles Dowek. 1009-1062
- Logical FrameworksFrank Pfenning. 1063-1147
- Proof-Assistants Using Dependent Type SystemsHenk Barendregt, Herman Geuvers. 1149-1238
- Nonmonotonic Reasoning: Towards Efficient Calculi and ImplementationsJürgen Dix, Ulrich Furbach, Ilkka Niemelä. 1241-1354
- Automated Deduction for Many-Valued LogicsMatthias Baaz, Christian G. Fermüller, Gernot Salzer. 1355-1402
- Encoding Two-Valued Nonclassical Logics in Classical LogicHans Jürgen Ohlbach, Andreas Nonnengart, Maarten de Rijke, Dov M. Gabbay. 1403-1486
- Connections in Nonclassical LogicsArild Waaler. 1487-1578
- Reasoning in Expressive Description LogicsDiego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, Daniele Nardi. 1581-1634
- Model CheckingEdmund M. Clarke, Bernd-Holger Schlingloff. 1635-1790
- Resolution Decision ProceduresChristian G. Fermüller, Alexander Leitsch, Ullrich Hustadt, Tanel Tammet. 1791-1849
- Term IndexingI. V. Ramakrishnan, R. C. Sekar, Andrei Voronkov. 1853-1964
- Combining Superposition, Sorts and SplittingChristoph Weidenbach. 1965-2013
- Model Elimination and Connection Tableau ProceduresReinhold Letz, Gernot Stenz. 2015-2114