Automated Deduction -- CADE 21

  • ISBN13:


  • ISBN10:


  • Format: Paperback
  • Copyright: 2007-09-03
  • Publisher: Springer-Verlag New York Inc
  • Purchase Benefits
  • Free Shipping On Orders Over $35!
    Your order must be $35 or more to qualify for free economy shipping. Bulk sales, PO's, Marketplace items, eBooks and apparel do not qualify for this offer.
  • Get Rewarded for Ordering Your Textbooks! Enroll Now
List Price: $119.99


This book constitutes the refereed proceedings of the 21st International Conference on Automated Deduction, CADE-21, held in Bremen, Germany, in July 2007. The 28 revised full papers and 6 system descriptions presented were carefully reviewed and selected from 64 submissions. All current aspects of automated deduction are addressed, ranging from theoretical and methodological issues to presentation and evaluation of theorem provers and logical reasoning systems. The papers are organized in topical sections on higher-order logic, description logic, intuitionistic logic, satisfiability modulo theories, induction, rewriting, and polymorphism, first-order logic, model checking and verification, termination, as well as tableaux and first-order systems.

Table of Contents

Invited Talk: Colin Stirling
Games, Automata and Matchingp. 1
Higher-Order Logic
Formalization of Continuous Probability Distributionsp. 3
Compilation as Rewriting in Higher Order Logicp. 19
Barendregt's Variable Convention in Rule Inductionsp. 35
Automating Elementary Number-Theoretic Proofs Using Grobner Basesp. 51
Description Logic
Optimized Reasoning in Description Logics Using Hypertableauxp. 67
Conservative Extensions in the Lightweight Description Logic ELp. 84
An Incremental Technique for Automata-Based Decision Proceduresp. 100
Intuitionistic Logic
Bidirectional Decision Procedures for the Intuitionistic Prepositional Modal Logic IS4p. 116
A Labelled System for IPL with Variable Splittingp. 132
Invited Talk: Ashish Tiwari
Logical Interpretation: Static Program Analysis Using Theorem Provingp. 147
Satisfiability Modulo Theories
Solving Quantified Verification Conditions Using Satisfiability Modulo Theoriesp. 167
Efficient E-Matching for SMT Solversp. 183
T-Decision by Decompositionp. 199
Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmeticp. 215
Induction, Rewriting, and Polymorphism
Improvements in Formula Generalizationp. 231
On the Normalization and Unique Normalization Properties of Term Rewrite Systemsp. 247
Handling Polymorphism in Automated Deductionp. 263
First-Order Logic
Automated Reasoning in Kleene Algebrap. 279
SRASS - A Semantic Relevance Axiom Selection Systemp. 295
Labelled Clausesp. 311
Automatic Decidability and Combinability Revisitedp. 328
Invited Talk: K. Rustan M. Leino
Designing Verification Conditions for Softwarep. 345
Model Checking and Verification
Encodings of Bounded LTL Model Checking in Effectively Propositional Logicp. 346
Combination Methods for Satisfiability and Model-Checking of Infinite-State Systemsp. 362
The KeY System 1.0p. 379
KeY-C: A Tool for Verification of C Programsp. 385
The Bedwyr System for Model Checking over Syntactic Expressionsp. 391
System for Automated Deduction (SAD): A Tool for Proof Verificationp. 398
Invited Talk: Peter Baumgartner
Logical Engineering with Instance-Based Methodsp. 404
Predictive Labeling with Dependency Pairs Using SATp. 410
Dependency Pairs for Rewriting with Non-free Constructorsp. 426
Proving Termination by Bounded Increasep. 443
Certified Size-Change Terminationp. 460
Tableaux and First-Order Systems
Encoding First Order Proofs in SATp. 476
Hyper Tableaux with Equalityp. 492
System Description: E-KRHyperp. 508
System Description: SPASS Version 3.0p. 514
Author Indexp. 521
Table of Contents provided by Ingram. All Rights Reserved.

Rewards Program

Write a Review