Automated deduction. A basis for applications. Vol. 2: Systems and implementation techniques (Q1581359)

The articles of this volume will be reviewed individually. For Vol. 1 see Zbl 0948.00014. Indexed articles: \textit{Reif, Wolfgang; Schellhorn, Gerhard; Stenzel, Kurt; Balser, Michael}, Structured specifications and interactive proofs with KIV, 13-39 [Zbl 0970.68149] \textit{Benl, Holger; Berger, Ulrich; Schwichtenberg, Helmut; Seisenberger, Monika; Zuber, Wolfgang}, Proof theory at work: Program development in the minlog system, 41-71 [Zbl 1015.68177] \textit{Strecker, Martin; Luther, Marko; von Henke, Friedrich}, Interactive and automated proof construction in type theory, 73-96 [Zbl 0970.68150] \textit{Ahrendt, Wolfgang; Beckert, Bernhard; Hähnle, Reiner; Menzel, Wolfram; Reif, Wolfgang; Schellhorn, Gerhard; Schmitt, Peter H.}, Integrating automated and interactive theorem proving, 97-123 [Zbl 0970.68151] \textit{Graf, Peter; Fehrer, Detlef}, Term indexing, 125-147 [Zbl 0970.68152] \textit{Fehrer, Detlef}, Developing deduction systems: The toolbox style, 149-166 [Zbl 0970.68153] \textit{Neugebauer, Gerd; Petermann, Uwe}, Specifications of inference rules: Extensions of the PTTP technique, 167-188 [Zbl 0973.68212] \textit{Kolbe, Thomas; Walther, Christoph}, Proof analysis, generalization and reuse, 189-229 [Zbl 0970.68154] \textit{Bündgen, Reinhard; Göbel, Manfred; Küchlin, Wolfgang; Weber, Andreas}, Parallel term rewriting with PaReDuX, 231-259 [Zbl 0973.68109] \textit{Schumann, Johann; Wolf, Andreas; Suttner, Christian}, Parallel theorem provers based on SETHEO, 261-290 [Zbl 0970.68155] \textit{Bornscheuer, Sven-Erik; Hölldobler, Steffen; Kalinke, Yvonne; Strohmaier, Antje}, Massively parallel reasoning, 291-329 [Zbl 1015.68541] \textit{Baaz, Matthias; Egly, Uwe; Leitsch, Alexander}, Extension methods in automated deduction, 331-359 [Zbl 0973.68214] \textit{Denzinger, Jörg; Fuchs, Matthias}, A comparison of equality reasoning heuristics, 361-382 [Zbl 0970.68156] \textit{Denzinger, Jörg; Dahn, Ingo}, Cooperating theorem provers, 383-416 [Zbl 0970.68157]