+612 9045 4394
Automated Deduction - CADE-21 : 21st International Conference on Automated Deduction Bremen, Germany, July 17-20, 2007 Proceedings - Frank Pfenning

Automated Deduction - CADE-21

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

By: Frank Pfenning (Editor)

Paperback Published: 5th July 2007
ISBN: 9783540735946
Number Of Pages: 522

Share This Book:


or 4 easy payments of $42.43 with Learn more
Ships in 7 to 10 business days

A veritable one-stop-shop for anyone looking to get up to speed on what is going down in the field of automated deduction right now. This book contains 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 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.

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.

ISBN: 9783540735946
ISBN-10: 3540735941
Series: Lecture Notes in Computer Science
Audience: General
Format: Paperback
Language: English
Number Of Pages: 522
Published: 5th July 2007
Publisher: Springer-Verlag Berlin and Heidelberg Gmbh & Co. Kg
Country of Publication: DE
Dimensions (cm): 23.8 x 16.13  x 3.15
Weight (kg): 0.84