Skip to main content
SpringerLink
Log in
Book cover

Automated Deduction – CADE-22

22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings

  • Conference proceedings
  • © 2009

Overview

Editors:
  1. Renate A. Schmidt

    1. School of Computer Science, The 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 5663)

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

Included in the following conference series:

Conference proceedings info: CADE 2009.

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 (35 papers)

  1. Front Matter

    Download chapter PDF

  3. Session 2. Combinations and Extensions

    1. Superposition and Model Evolution Combined

      • Peter Baumgartner, Uwe Waldmann
      Pages 17-34

    2. On Deciding Satisfiability by DPLL(\(\Gamma+{\mathcal T}\)) and Unsound Theorem Proving

      • Maria Paola Bonacina, Christopher Lynch, Leonardo de Moura
      Pages 35-50

    3. Combinable Extensions of Abelian Groups

      • Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch
      Pages 51-66

    4. Locality Results for Certain Extensions of Theories with Bridging Functions

      • Viorica Sofronie-Stokkermans
      Pages 67-83

  4. Session 3. Minimal Unsatisfiability and Automated Reasoning Support

    1. Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis

      • Roberto Sebastiani, Michele Vescovi
      Pages 84-99

    2. Does This Set of Clauses Overlap with at Least One MUS?

      • Éric Grégoire, Bertrand Mazure, Cédric Piette
      Pages 100-115

    3. Progress in the Development of Automated Theorem Proving for Higher-Order Logic

      • Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, Frank Theiss
      Pages 116-130

  5. Session 4. System Descriptions

    1. System Description: H-PILoT

      • Carsten Ihlemann, Viorica Sofronie-Stokkermans
      Pages 131-139

    2. SPASS Version 3.5

      • Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, Patrick Wischnewski
      Pages 140-145

    3. Dei: A Theorem Prover for Terms with Integer Exponents

      • Hicham Bensaid, Ricardo Caferra, Nicolas Peltier
      Pages 146-150

    4. veriT: An Open, Trustable and Efficient SMT-Solver

      • Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine
      Pages 151-156

    5. Divvy: An ATP Meta-system Based on Axiom Relevance Ordering

      • Alex Roederer, Yury Puzis, Geoff Sutcliffe
      Pages 157-162

  6. Session 5. Invited Talk

    1. Instantiation-Based Automated Reasoning: From Theory to Practice

      • Konstantin Korovin
      Pages 163-166

  7. Session 6. Interpolation and Predicate Abstraction

    1. Interpolant Generation for UTVPI

      • Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani
      Pages 167-182

    2. Ground Interpolation for Combined Theories

      • Amit Goel, Sava Krstić, Cesare Tinelli
      Pages 183-198

    3. Interpolation and Symbol Elimination

      • Laura Kovács, Andrei Voronkov
      Pages 199-213

    4. Complexity and Algorithms for Monomial and Clausal Predicate Abstraction

      • Shuvendu K. Lahiri, Shaz Qadeer
      Pages 214-229

  8. Session 7. Resolution-Based Systems for Non-classical Logics

    1. Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method

      • Sean McLaughlin, Frank Pfenning
      Pages 230-244
Back to top

Other volumes

  1. Automated Deduction – CADE-22

Keywords

About this book

This book constitutes the refereed proceedings of the 22nd International Conference on Automated Deduction, CADE-22, held in Montreal, Canada, in August 2009.

The 27 revised full papers and 5 system descriptions presented were carefully reviewed and selected from 77 submissions. Furthermore, three invited lectures by distinguished experts in the area were included. The papers are organized in topical sections on combinations and extensions, minimal unsatisfiability and automated reasoning support, system descriptions, interpolation and predicate abstraction, resolution-based systems for non-classical logics, termination analysis and constraint solving, rewriting, termination and productivity, models, modal tableaux with global caching, arithmetic.

Editors and Affiliations

  • School of Computer Science, The University of Manchester, Manchester, UK

    Renate A. Schmidt

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation