Volume I: Foundations. Calculi and Methods. Preface; W. Bibel, P.H. Schmitt. Part One: Tableau and Connection Calculi. Introduction; U. Furbach. 1. Analytic Tableaux; B. Beckert, R. Hähnle. 2. Clausal Tableaux; R. Letz. 3. Variants of Clausal Tableaux; P. Baumgartner, U. Furbach. 4. Cuts in Tableaux; U. Egly. 5. Compressions and Extensions; W. Bibel, et al. Part Two: Special Calculi and Refinements. Introduction; U. Petermann. 6. Theory Reasoning; P. Baumgartner, U. Petermann. 7. Unification Theory; F. Baader, K.U. Schulz. 8. Rigid E-Unification; B. Beckert. 9. Sorted Unification and Tree Automata; C. Weidenbach. 10. Dimensions of Types in Logic Programming; G. Meyer, C. Beierle. 11. Equational Reasoning in Saturation-Based Theorem Proving; L. Bachmair, H. Ganzinger. 12. Higher-Order Rewriting and Equational Reasoning; T. Nipkow, C. Prehofer. 13. Higher-Order Automated Theorem Proving; M. Kohlhase. Index. Volume II: Systems and Implementation Techniques. Introduction; T. Nipkow, W. Reif. 1. Structured Specifications and Interactive Proofs with KIV; W. Reif, et al. 2. Proof Theory at Work: Program Development in the Minlog System; H. Benl, et al. 3. Interactive and Automated Proof Construction in Type Theory; M. Strecker, et al. 4. Integrating Automated and Interactive Theorem Proving; W. Ahrendt, et al. PartTwo: Representation and Optimization Techniques. Introduction; J. Siekmann, D. Fehrer. 5. Term Indexing; P. Graf, D. Fehrer. 6. Developing Deduction Systems: The Toolbox Style; D. Fehrer. 7. Specifications of Inference Rules: Extensions of the PTTP Technique; G. Neugebauer, U. Petermann. 8. Proof Analysis, Generalization and Reuse; T. Kolbe, C. Walther. Part Three: Parallel Inference Systems. Introduction; W. Küchlin. 9. Parallel Term Rewriting with PaReDuX; R. Bündgen, et al. 10. Parallel Theorem Provers Based on SETHEO; J. Schumann, et al. 11. Massively Parallel Reasoning; S.-E. Bornscheuer, et al. Part Four: Comparison and Cooperation of Theorem Provers. Introduction; J. Avenhaus. 12. Extension Methods in Automated Deduction; M. Baaz, et al. 13. A Comparison of Equality Reasoning Heuristics; J. Denzinger, M. Fuchs. 14. Cooperating Theorem Provers; J. Denzinger, I. Dahn. Index. Volume III: Applications. Part One: Automated Theorem Proving in Mathematics. Introduction; M. Kohlhase. 1. Lattice-Ordered Groups in Deduction; I. Dahn. 2. Superposition Theorem Proving for Commutative Rings; J. Stuber. 3. How to Augment a Formal System with a Boolean Algebra Component; H.J. Ohlbach, J. Kühler. 4. Proof Planning: A practical Approach to Mechanized Reasoning in Mathematics; M. Kerber. Part Two: Automated Deduction in Software Engineering and hardware Design. Introduction; J. Schum