Skip to main content
SpringerLink
Log in

Automated Deduction - CADE-21

21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings

  • Conference proceedings
  • © 2007

Overview

Editors:
  1. Frank Pfenning
    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 4603)

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

Included in the following conference series:

Conference proceedings info: CADE 2007.

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

  1. Session 8. First-Order Logic

    1. SRASS - A Semantic Relevance Axiom Selection System

      • Geoff Sutcliffe, Yury Puzis
      Pages 295-310

    2. Labelled Clauses

      • Tal Lev-Ami, Christoph Weidenbach, Thomas Reps, Mooly Sagiv
      Pages 311-327

    3. Automatic Decidability and Combinability Revisited

      • Christopher Lynch, Duc-Khanh Tran
      Pages 328-344

  2. Session 9. Invited Talk: K. Rustan M. Leino

    1. Designing Verification Conditions for Software

      • K. Rustan M. Leino
      Pages 345-345

  3. Session 10. Model Checking and Verification

    1. Encodings of Bounded LTL Model Checking in Effectively Propositional Logic

      • Juan Antonio Navarro-Pérez, Andrei Voronkov
      Pages 346-361

    2. Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems

      • Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli
      Pages 362-378

    3. The KeY system 1.0 (Deduction Component)

      • Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Philipp Rümmer, Steffen Schlager et al.
      Pages 379-384

    4. KeY-C: A Tool for Verification of C Programs

      • Oleg Mürk, Daniel Larsson, Reiner Hähnle
      Pages 385-390

    5. The Bedwyr System for Model Checking over Syntactic Expressions

      • David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu
      Pages 391-397

    6. System for Automated Deduction (SAD): A Tool for Proof Verification

      • Konstantin Verchinine, Alexander Lyaletski, Andrei Paskevich
      Pages 398-403

  4. Session 11. Invited Talk: Peter Baumgartner

    1. Logical Engineering with Instance-Based Methods

      • Peter Baumgartner
      Pages 404-409

  5. Session 12. Termination

    1. Predictive Labeling with Dependency Pairs Using SAT

      • Adam Koprowski, Aart Middeldorp
      Pages 410-425

    2. Dependency Pairs for Rewriting with Non-free Constructors

      • Stephan Falke, Deepak Kapur
      Pages 426-442

    3. Proving Termination by Bounded Increase

      • Jürgen Giesl, René Thiemann, Stephan Swiderski, Peter Schneider-Kamp
      Pages 443-459

    4. Certified Size-Change Termination

      • Alexander Krauss
      Pages 460-475

  6. Session 13. Tableaux and First-Order Systems

    1. Encoding First Order Proofs in SAT

      • Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin, Christopher Lynch, Ralph Eric McGregor
      Pages 476-491

    2. Hyper Tableaux with Equality

      • Peter Baumgartner, Ulrich Furbach, Björn Pelzer
      Pages 492-507

    3. System Description: E- KRHyper

      • Björn Pelzer, Christoph Wernhard
      Pages 508-513

    4. System Description: Spass Version 3.0

      • Christoph Weidenbach, Renate A. Schmidt, Thomas Hillenbrand, Rostislav Rusev, Dalibor Topic
      Pages 514-520

  7. Back Matter

    Download chapter PDF
Back to top

Other volumes

  1. Automated Deduction – CADE-21

Keywords

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation