Automated Deduction - CADE-18

1. Front Matter

   Pages I-XII

   PDF

2. Description Logics and Semantic Web

   1. Reasoning with Expressive Description Logics: Theory and Practice

      • Ian Horrocks

      Pages 1-15

   2. BDD-Based Decision Procedures for \( \mathcal{K} \)

      • Guoqiang Pan, Ulrike Sattler, Moshe Y. Vardi

      Pages 16-30

3. Proof-Carrying Code and Compiler Verification

   1. Temporal Logic for Proof-Carrying Code

      • Andrew Bernard, Peter Lee

      Pages 31-46

   2. A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code

      • Robert R. Schneck, George C. Necula

      Pages 47-62

   3. Formal Verification of a Java Compiler in Isabelle

      • Martin Strecker

      Pages 63-77

4. Non-classical Logics

   1. Embedding Lax Logic into Intuitionistic Logic

      • Uwe Egly

      Pages 78-93

   2. Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic

      • Dominique Larchey-Wendling

      Pages 94-110

   3. Connection-Based Proof Search in Propositional BI Logic

      • Didier Galmiche, Daniel Méry

      Pages 111-128

5. System Descriptions

   1. DDDLIB: A Library for Solving Quantified Difference Inequalities

      • Jesper B. Møller

      Pages 129-133

   2. An LCF-Style Interface between HOL and First-Order Logic

      • Joe Hurd

      Pages 134-138

   3. System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning

      • Jürgen Zimmer, Michael Kohlhase

      Pages 139-143

   4. Proof Development with Ωmega

      • Jörg Siekmann, Christoph Benzmüller, Vladimir Brezhnev, Lassaad Cheikhrouhou, Armin Fiedler, Andreas Franke et al.

      Pages 144-149

   5. LearnΩmatic: System Description

      • Mateja Jamnik, Manfred Kerber, Martin Pollet

      Pages 150-155

   6. HyLoRes 1.0: Direct Resolution for Hybrid Logics

      • Carlos Areces, Juan Heguiabehere

      Pages 156-160

6. SAT

   1. Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points

      • Eugene Goldberg

      Pages 161-180

   2. A Note on Symmetry Heuristics in SEM

      • Thierry Boy de la Tour

      Pages 181-194

   3. A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions

      • Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Korniłowicz, Roberto Sebastiani

      Pages 195-210

7. Model Generation

   1. Deductive Search for Errors in Free Data Type Specifications Using Model Generation

      • Wolfgang Ahrendt

      Pages 211-225

   2. Reasoning by Symmetry and Function Ordering in Finite Model Generation

      • Gilles Audemard, Belaid Benhamou

      Pages 226-240

The First CADE in the Third Millennium This volume contains the papers presented at the Eighteenth International C- ference on Automated Deduction (CADE-18) held on July 27–30th, 2002, at the University of Copenhagen as part of the Federated Logic Conference (FLoC 2002). Despite a large number of deduction-related conferences springing into existence at the end of the last millennium, the CADE conferences continue to be the major forum for the presentation of new research in all aspects of automated deduction. CADE-18 was sponsored by the Association for Auto- ted Reasoning, CADE Inc., the Department of Computer Science at Chalmers University, the Gesellschaft fur ¨ Informatik, Safelogic AB, and the University of Koblenz-Landau. There were 70 submissions, including 60 regular papers and 10 system - scriptions. Each submission was reviewed by at least ?ve program committee members and an electronic program committee meeting was held via the Int- net. The committee decided to accept 27 regular papers and 9 system descr- tions. One paper switched its category after refereeing, thus the total number of system descriptions in this volume is 10. In addition to the refereed papers, this volume contains an extended abstract of the CADE invited talk by Ian Horrocks, the joint CADE/CAV invited talk by Sharad Malik, and the joint CADE-TABLEAUX invited talk by Matthias Baaz. One more invited lecture was given by Daniel Jackson.

• Automat
• automated deduction
• compiler
• description logics
• proof theory
• semantic web
• verification

• Department of Computer Science, University of Manchester, Manchester, UK

  Andrei Voronkov

Policies and ethics