Skip to main content
SpringerLink
Log in

Automated Deduction - CADE-18

18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002 Proceedings

  • Conference proceedings
  • © 2002

Overview

Editors:
  1. Andrei Voronkov

    1. Department of Computer Science, University of Manchester, Manchester, UK

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 2392)

Part of the book sub series: Lecture Notes in Artificial Intelligence (LNAI)

Included in the following conference series:

Conference proceedings info: CADE 2002.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (40 papers)

  1. Front Matter

    Pages I-XII
    Download chapter 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
Back to top

Other volumes

  1. Automated Deduction—CADE-18

Keywords

About this book

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.

Editors and Affiliations

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

    Andrei Voronkov

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation