Automated deduction - CADE-15. 15th international conference, Lindau, Germany, July 5--10, 1998. Proceedings
type: Item
instance of: scholarly article
title: Automated deduction - CADE-15. 15th international conference, Lindau, Germany, July 5--10, 1998. Proceedings
zbMATH Open document ID: 0892.00047
published in: Lecture Notes in Computer Science
publication date: 1998-07-13T00:00:00Z
review text: 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.0…
Mathematics Subject Classification ID: 00B25
Mathematics Subject Classification ID: 03-06
Mathematics Subject Classification ID: 68-06
zbMATH DE Number: 1174014
zbMATH Keywords: Lindau (Germany)
zbMATH Keywords: Proceedings
zbMATH Keywords: Conference
zbMATH Keywords: CADE-15
MaRDI profile type: Publication
DOI: 10.1007/BFB0054239
description: scientific article; zbMATH DE number 1174014