
Conferences in DBLP
 Frank Pfenning
Reasoning About Deductions in Linear Logic (Abstract of Invited Talk). [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:12 [Conf]
 Jacques D. Fleuriot, Lawrence C. Paulson
A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:316 [Conf]
 Stéphane Fèvre, Dongming Wang
Proving Geometric Theorems Using Clifford Algebra and Rewrite Rules. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:1731 [Conf]
 Marc Fuchs
System Description: SimilarityBased Lemma Generation for Model Elimination. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:3337 [Conf]
 Thomas Arts, Mads Dam, LarsÅke Fredlund, Dilian Gurov
System Description: Verification of Distributed Erlang Programs. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:3841 [Conf]
 Marc Fuchs, Andreas Wolf
System Description: Cooperation in Model Elimination: CPTHEO. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:4246 [Conf]
 Rajeev Goré, Joachim Posegga, Andrew Slater, Harald Vogt
System Description: card T^{A}P: The First Theorem Prover on a Smart Card. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:4750 [Conf]
 Bernhard Beckert, Rajeev Goré
System Description: leanK 2.0. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:5155 [Conf]
 Christoph Benzmüller, Michael Kohlhase
Extensional HigherOrder Resolution. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:5671 [Conf]
 Bruno Pagano
X.R.S : Explicit Reduction Systems  A FirstOrder Calculus for HigherOrder Calculi. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:7287 [Conf]
 Alexandre Boudet, Evelyne Contejean
About the Confluence of Equational Pattern Rewrite Systems. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:88102 [Conf]
 Michael Beeson
Unification in LambdaCalculi with ifthenelse. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:103118 [Conf]
 Nicolas Peltier
System Description: An Equational Constraints Solver. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:119123 [Conf]
 Bertrand Mazure, Lakhdar Sais, Éric Grégoire
System Description: CRIL Platform for SAT. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:124128 [Conf]
 Julian Richardson, Alan Smaill, Ian Green
System Description: Proof Planning in HigherOrder Logic with LambdaClam. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:129133 [Conf]
 Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy
System Description: An Interface Between CL^{A}M and HOL. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:134138 [Conf]
 Christoph Benzmüller, Michael Kohlhase
System Description: LEO  A HigherOrder Theorem Prover. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:139144 [Conf]
 Uwe Waldmann
Superposition for Divisible TorsionFree Abelian Groups. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:144159 [Conf]
 Leo Bachmair, Harald Ganzinger
Strict Basic Superposition. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:160174 [Conf]
 Leo Bachmair, Harald Ganzinger, Andrei Voronkov
Elimination of Equality via Transformation with Ordering Constraints. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:175190 [Conf]
 Hans de Nivelle
A Resolution Decision Procedure for the Guarded Fragment. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:191204 [Conf]
 Hans Jürgen Ohlbach
Combining Hilbert Style and Semantic Reasoning in a Resolution Framework. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:205219 [Conf]
 Matt Kaufmann
ACL2 Support for Verification Projects (Invited Talk). [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:220238 [Conf]
 Alberto Oliart, Wayne Snyder
A Fast Algorithm for Uniform SemiUnification. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:239253 [Conf]
 Jürgen Brauburger, Jürgen Giesl
Termination Analysis by Inductive Evaluation. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:254269 [Conf]
 Karl Crary
Admissibility of Fixpoint Induction over Partial Types. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:270285 [Conf]
 Carsten Schürmann, Frank Pfenning
Automated Theorem Proving in a Simple MetaLogic for LF. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:286300 [Conf]
 Amir Pnueli
Deductive vs. ModelTheoretic Approaches to Formal Verification (Abstract of Invited Talk). [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:301 [Conf]
 Robi Malik
Automated Deduction of FiniteState Control Programs for Reactive Systems. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:302316 [Conf]
 Christoph Kreitz, Mark Hayden, Jason Hickey
A Proof Environment for the Development of Group Communication Systems. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:317332 [Conf]
 Yoshihiko Ohta, Katsumi Inoue, Ryuzo Hasegawa
On the Relationship Between NonHorn Magic Sets and Relevancy Testing. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:333348 [Conf]
 Laurent Théry
A Certified Version of Buchberger's Algorithm. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:349364 [Conf]
 Matthew Bishop, Peter B. Andrews
Selectively Instantiating Definitions. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:365380 [Conf]
 Reinhold Letz
Using Matings for Pruning Connection Tableaux. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:381396 [Conf]
 Andreas Nonnengart, Georg Rock, Christoph Weidenbach
On Generating Small Clause Normal Forms. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:397411 [Conf]
 Joseph Douglas Horton, Bruce Spencer
Rank/Activity: A Canonical Form for Binary Resolution. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:412426 [Conf]
 Tanel Tammet
Towards Efficient Subsumption. [Citation Graph (0, 0)][DBLP] CADE, 1998, pp:427441 [Conf]
