Automated deduction - CADE-15. 15th international conference, Lindau, Germany, July 5--10, 1998. Proceedings (Q1389909)

The articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1415.68038]. Indexed articles: \textit{Fleuriot, Jacques D.; Paulson, Lawrence C.}, A combination of nonstandard analysis and geometry theorem proving, with application to Newton's Principia, 3-16 [Zbl 0924.03022] \textit{Fèvre, Stéphane; Wang, Dongming}, Proving geometric theorems using Clifford algebra and rewrite rules, 17-32 [Zbl 0924.03021] \textit{Benzmüller, Christoph; Kohlhase, Michael}, Extensional higher-order resolution, 56-71 [Zbl 0928.03004] \textit{Pagano, Bruno}, X. R. S. : Explicit reduction systems -- A first-order calculus for higher-order calculi, 72-87 [Zbl 0924.03047] \textit{Boudet, Alexandre; Contejean, Evelyne}, About the confluence of equational pattern rewrite systems, 88-102 [Zbl 0924.03041] \textit{Beeson, Michael}, Unification in lambda-calculi with if-then-else, 103-118 [Zbl 0924.03018] \textit{Waldmann, Uwe}, Superposition for divisible torsion-free abelian groups, 144-159 [Zbl 0924.03026] \textit{Bachmair, Leo; Ganzinger, Harald}, Strict basic superposition, 160-174 [Zbl 0924.03017] \textit{Bachmair, Leo; Ganzinger, Harald; Voronkov, Andrei}, Elimination of equality via transformation with ordering constraints, 175-190 [Zbl 0926.03006] \textit{de Nivelle, Hans}, A resolution decision procedure for the guarded fragment, 191-204 [Zbl 0927.03027] \textit{Ohlbach, Hans Jürgen}, Combining Hilbert style and semantic reasoning in a resolution framework, 205-219 [Zbl 0928.03011] \textit{Crary, Karl}, Admissibility of fixpoint induction over partial types, 270-285 [Zbl 0924.03019] \textit{Schürmann, Carsten; Pfenning, Frank}, Automated theorem proving in a simple meta-logic for LF, 286-300 [Zbl 0924.03024] \textit{Ohta, Yoshihiko; Inoue, Katsumi; Hasegawa, Ryuzo}, On the relationship between non-Horn magic sets and relevancy testing, 333-348 [Zbl 0926.03008] \textit{Théry, Laurent}, A certified version of Buchberger's algorithm, 349-364 [Zbl 0924.03025] \textit{Nonnengart, Andreas; Rock, Georg; Weidenbach, Christoph}, On generating small clause normal forms, 397-411 [Zbl 0924.03023] \textit{Horton, J. D.; Spencer, Bruce}, Rank/activity: A canonical form for binary resolution, 412-426 [Zbl 0926.03007]