Automated deduction. A basis for applications. Vol. III: Applications (Q1581357)

The articles of this volume will be reviewed individually. Indexed articles: \textit{Dahn, Ingo}, Lattice-ordered groups in deduction, 9-29 [Zbl 0969.03021] \textit{Stuber, Jürgen}, Superposition theorem proving for commutative rings, 31-55 [Zbl 0970.03022] \textit{Ohlbach, Hans Jürgen; Köhler, Jana}, How to augment a formal system with a Boolean algebra component, 57-75 [Zbl 0967.03011] \textit{Kerber, Manfred}, Proof planning: A practical approach to mechanized reasoning in mathematics, 77-104 [Zbl 0967.03010] \textit{Kreitz, Christoph}, Program synthesis, 105-134 [Zbl 0972.68514] \textit{Giesl, Jürgen; Walther, Christoph; Brauburger, Jürgen}, Termination analysis for functional programs, 135-164 [Zbl 0972.68031] \textit{Schellhorn, Gerhard; Ahrendt, Wolfgang}, The WAM case study: Verifying compiler correctness for Prolog with KIV, 165-194 [Zbl 0977.68017] \textit{Dahn, Ingo; Schumann, Johann}, Using automated theorem provers in verification of protocols, 195-224 [Zbl 0972.68011] \textit{Reif, Wolfgang; Schellhorn, Gerhard}, Theorem proving in large theories, 225-241 [Zbl 0972.68520] \textit{Stolzenburg, Frieder; Thomas, Bernd}, Analyzing rule sets for the calculation of banking fees by a theorem prover with constraints, 243-264 [Zbl 0972.68144] \textit{Fischer, Bernd; Schumann, Johann; Snelting, Gregor}, Deduction-based software component retrieval, 265-292 [Zbl 0972.68042] \textit{Bündgen, Reinhard}, Rewrite based hardware verification with ReDuX, 293-316 [Zbl 0972.68145]