Automated deduction. A basis for applications. Vol. 1: Foundations, calculi and methods (Q1581358)

The articles of this volume will be reviewed individually. For Vol. 2 see Zbl 0948.00015. Indexed articles: \textit{Beckert, Bernhard; Hähnle, Reiner}, Analytic tableaux, 11-41 [Zbl 0971.03018] \textit{Letz, Reinhold}, Clausal tableaux, 43-72 [Zbl 0966.03013] \textit{Baumgartner, Peter; Furbach, Ulrich}, Variants of clausal tableaux, 73-101 [Zbl 0977.68076] \textit{Egly, Uwe}, Cuts in tableaux, 103-131 [Zbl 0971.03015] \textit{Bibel, Wolfgang; Brüning, Stefan; Otten, Jens; Rath, Thomas; Schaub, Torsten}, Compressions and extensions, 133-190 [Zbl 0971.03014] \textit{Baumgartner, Peter; Petermann, Uwe}, Theory reasoning, 191-224 [Zbl 0968.03017] \textit{Baader, Franz; Schulz, Klaus U.}, Unification theory, 225-263 [Zbl 0970.68148] \textit{Beckert, Bernhard}, Rigid \(E\)-unification, 265-289 [Zbl 0973.68213] \textit{Weidenbach, Christoph}, Sorted unification and tree automata, 291-320 [Zbl 0970.68095] \textit{Meyer, Gregor; Beierle, Christoph}, Dimensions of types in logic programming, 321-351 [Zbl 0973.68032] \textit{Bachmair, Leo; Ganzinger, Harald}, Equational reasoning in saturation-based theorem proving, 353-397 [Zbl 0973.68215] \textit{Nipkow, Tobias; Prehofer, Christian}, Higher-order rewriting and equational reasoning, 399-430 [Zbl 0970.68081] \textit{Kohlhase, Michael}, Higher-order automated theorem proving, 431-462 [Zbl 0971.68141]