18. CADE 2002: Copenhagen, Denmark

Description Logics and Semantic Web

• Ian Horrocks:
  Reasoning with Expressive Description Logics: Theory and Practice. 1-15
  
• Guoqiang Pan, Ulrike Sattler, Moshe Y. Vardi:
  BDD-Based Decision Procedures for K. 16-30
  

Proof-Carrying Code and Compiler Verification

• Andrew Bernard, Peter Lee:
  Temporal Logic for Proof-Carrying Code. 31-46
  
• Robert R. Schneck, George C. Necula:
  A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code. 47-62
  
• Martin Strecker:
  Formal Verification of a Java Compiler in Isabelle. 63-77
  

Non-classical Logics

• Uwe Egly:
  Embedding Lax Logic into Intuitionistic Logic. 78-93
  
• Dominique Larchey-Wendling:
  Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic. 94-110
  
• Didier Galmiche, Daniel Méry:
  Connection-Based Proof Search in Propositional BI Logic. 111-128
  

System Descriptions

• Jesper B. Møller:
  DDDLIB: A Library for Solving Quantified Difference Inequalities. 129-133
  
• Joe Hurd:
  An LCF-Style Interface between HOL and First-Order Logic. 134-138
  
• Jürgen Zimmer, Michael Kohlhase:
  System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning. 139-143
  
• Jörg H. Siekmann, Christoph Benzmüller, Vladimir Brezhnev, Lassaad Cheikhrouhou, Armin Fiedler, Andreas Franke, Helmut Horacek, Michael Kohlhase, Andreas Meier, Erica Melis, Markus Moschner, Immanuel Normann, Martin Pollet, Volker Sorge, Carsten Ullrich, Claus-Peter Wirth, Jürgen Zimmer:
  Proof Development with OMEGA. 144-149
  
• Mateja Jamnik, Manfred Kerber, Martin Pollet:
  Learn Omega-matic: System Description. 150-155
  
• Carlos Areces, Juan Heguiabehere:
  HyLoRes 1.0: Direct Resolution for Hybrid Logics. 156-160
  

SAT

• Eugene Goldberg:
  Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points. 161-180
  
• Thierry Boy de la Tour:
  A Note on Symmetry Heuristics in SEM. 181-194
  
• Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani:
  A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. 195-210
  

Model Generation

• Wolfgang Ahrendt:
  Deductive Search for Errors in Free Data Type Specifications Using Model Generation. 211-225
  
• Gilles Audemard, Belaid Benhamou:
  Reasoning by Symmetry and Function Ordering in Finite Model Generation. 226-240
  
• Bernhard Gramlich, Reinhard Pichler:
  Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations. 241-259
  

• Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt:
  A New Clausal Class Decidable by Hyperresolution. 260-274
  

CASC

• Christoph Weidenbach, Uwe Brahm, Thomas Hillenbrand, Enno Keen, Christian Theobald, Dalibor Topic:
  S PASS Version 2.0. 275-279
  
• Stephan Schulz, Geoff Sutcliffe:
  System Description: GrAnDe 1.0. 280-284
  
• Simon Colton:
  The HR Program for Theorem Generation. 285-289
  
• Michael W. Whalen, Johann Schumann, Bernd Fischer:
  AutoBayes/CC - Combining Program Synthesis with Automatic Code Certification - System Description. 290-294
  

CADE-CAV Invited Talk

• Lintao Zhang, Sharad Malik:
  The Quest for Efficient Boolean Satisfiability Solvers. 295-313
  

• Cristina Borralleras, Salvador Lucas, Albert Rubio:
  Recursive Path Orderings Can Be Context-Sensitive. 314-331
  

Combination of Decision Procedures

• Harald Ganzinger:
  Shostak Light. 332-346
  
• Jonathan Ford, Natarajan Shankar:
  Formal Verification of a Combination Decision Procedure. 347-362
  
• Calogero G. Zarba:
  Combining Multisets with Integers. 363-376
  

Logical Frameworks

• Lawrence C. Paulson:
  The Reflection Theorem: A Study in Meta-theoretic Reasoning. 377-391
  
• Aaron Stump, David L. Dill:
  Faster Proof Checking in the Edinburgh Logical Framework. 392-407
  
• Chad E. Brown:
  Solving for Set Variables in Higher-Order Theorem Proving. 408-422
  

Model Checking

• Orna Kupferman, Ulrike Sattler, Moshe Y. Vardi:
  The Complexity of the Graded µ-Calculus. 423-437
  
• Leonardo Mendonça de Moura, Harald Rueß, Maria Sorea:
  Lazy Theorem Proving for Bounded Model Checking over Infinite Domains. 438-455
  

Equational Reasoning

• Miquel Bofill, Albert Rubio:
  Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation. 456-470
  
• Christopher Lynch, Barbara Morawska:
  Basic Syntactic Mutation. 471-485
  
• Thomas Hillenbrand, Bernd Löchner:
  The Next W ALDMEISTER Loop. 486-500
  

Proof Theory

• Jean-Marc Andreoli:
  Focussing Proof-Net Construction as a Middleware Paradigm. 501-516
  
• Matthias Baaz:
  Proof Analysis by Resolution. 517-532