15. CADE 1998: Lindau, Germany

Session 1:

• Frank Pfenning:
  Reasoning About Deductions in Linear Logic (Abstract of Invited Talk). 1-2
  
• Jacques D. Fleuriot, Lawrence C. Paulson:
  A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia. 3-16
  
• Stéphane Fèvre, Dongming Wang:
  Proving Geometric Theorems Using Clifford Algebra and Rewrite Rules. 17-31
  

Session 2: System Descriptions

• Marc Fuchs:
  System Description: Similarity-Based Lemma Generation for Model Elimination. 33-37
  
• Thomas Arts, Mads Dam, Lars-Åke Fredlund, Dilian Gurov:
  System Description: Verification of Distributed Erlang Programs. 38-41
  
• Marc Fuchs, Andreas Wolf:
  System Description: Cooperation in Model Elimination: CPTHEO. 42-46
  
• Rajeev Goré, Joachim Posegga, Andrew Slater, Harald Vogt:
  System Description: card T^AP: The First Theorem Prover on a Smart Card. 47-50
  
• Bernhard Beckert, Rajeev Goré:
  System Description: leanK 2.0. 51-55
  

Session 3:

• Christoph Benzmüller, Michael Kohlhase:
  Extensional Higher-Order Resolution. 56-71
  
• Bruno Pagano:
  X.R.S : Explicit Reduction Systems - A First-Order Calculus for Higher-Order Calculi. 72-87
  
• Alexandre Boudet, Evelyne Contejean:
  About the Confluence of Equational Pattern Rewrite Systems. 88-102
  

Session 4:

• Michael Beeson:
  Unification in Lambda-Calculi with if-then-else. 103-118
  

System Descriptions

• Nicolas Peltier:
  System Description: An Equational Constraints Solver. 119-123
  
• Bertrand Mazure, Lakhdar Sais, Éric Grégoire:
  System Description: CRIL Platform for SAT. 124-128
  
• Julian Richardson, Alan Smaill, Ian Green:
  System Description: Proof Planning in Higher-Order Logic with Lambda-Clam. 129-133
  
• Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy:
  System Description: An Interface Between CL^AM and HOL. 134-138
  
• Christoph Benzmüller, Michael Kohlhase:
  System Description: LEO - A Higher-Order Theorem Prover. 139-144
  

Session 5:

• Uwe Waldmann:
  Superposition for Divisible Torsion-Free Abelian Groups. 144-159
  
• Leo Bachmair, Harald Ganzinger:
  Strict Basic Superposition. 160-174
  
• Leo Bachmair, Harald Ganzinger, Andrei Voronkov:
  Elimination of Equality via Transformation with Ordering Constraints. 175-190
  

Session 6:

• Hans de Nivelle:
  A Resolution Decision Procedure for the Guarded Fragment. 191-204
  
• Hans Jürgen Ohlbach:
  Combining Hilbert Style and Semantic Reasoning in a Resolution Framework. 205-219
  

Session 7:

• Matt Kaufmann:
  ACL2 Support for Verification Projects (Invited Talk). 220-238
  
• Alberto Oliart, Wayne Snyder:
  A Fast Algorithm for Uniform Semi-Unification. 239-253
  

Session 8:

• Jürgen Brauburger, Jürgen Giesl:
  Termination Analysis by Inductive Evaluation. 254-269
  
• Karl Crary:
  Admissibility of Fixpoint Induction over Partial Types. 270-285
  
• Carsten Schürmann, Frank Pfenning:
  Automated Theorem Proving in a Simple Meta-Logic for LF. 286-300
  

Session 9:

• Amir Pnueli:
  Deductive vs. Model-Theoretic Approaches to Formal Verification (Abstract of Invited Talk). 301
  
• Robi Malik:
  Automated Deduction of Finite-State Control Programs for Reactive Systems. 302-316
  

Session 10:

• Christoph Kreitz, Mark Hayden, Jason Hickey:
  A Proof Environment for the Development of Group Communication Systems. 317-332
  
• Yoshihiko Ohta, Katsumi Inoue, Ryuzo Hasegawa:
  On the Relationship Between Non-Horn Magic Sets and Relevancy Testing. 333-348
  
• Laurent Théry:
  A Certified Version of Buchberger's Algorithm. 349-364
  

Session 11:

• Matthew Bishop, Peter B. Andrews:
  Selectively Instantiating Definitions. 365-380
  
• Reinhold Letz:
  Using Matings for Pruning Connection Tableaux. 381-396
  

Session 12:

• Andreas Nonnengart, Georg Rock, Christoph Weidenbach:
  On Generating Small Clause Normal Forms. 397-411
  
• Joseph Douglas Horton, Bruce Spencer:
  Rank/Activity: A Canonical Form for Binary Resolution. 412-426
  
• Tanel Tammet:
  Towards Efficient Subsumption. 427-441