Automated Deduction - CADE-21: 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings (Lecture Notes in Computer Science, 4603)

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. Front Matter....Pages - Games, Automata and Matching....Pages 1-2 Formalization of Continuous Probability Distributions....Pages 3-18 Compilation as Rewriting in Higher Order Logic....Pages 19-34 Barendregt’s Variable Convention in Rule Inductions....Pages 35-50 Automating Elementary Number-Theoretic Proofs Using Gröbner Bases....Pages 51-66 Optimized Reasoning in Description Logics Using Hypertableaux....Pages 67-83 Conservative Extensions in the Lightweight Description Logic $\mathcal{EL}$ ....Pages 84-99 An Incremental Technique for Automata-Based Decision Procedures....Pages 100-115 Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4 ....Pages 116-131 A Labelled System for IPL with Variable Splitting....Pages 132-146 Logical Interpretation: Static Program Analysis Using Theorem Proving....Pages 147-166 Solving Quantified Verification Conditions Using Satisfiability Modulo Theories....Pages 167-182 Efficient E-Matching for SMT Solvers....Pages 183-198 ${\mathcal{T}}$ -Decision by Decomposition....Pages 199-214 Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic....Pages 215-230 Improvements in Formula Generalization....Pages 231-246 On the Normalization and Unique Normalization Properties of Term Rewrite Systems....Pages 247-262 Handling Polymorphism in Automated Deduction....Pages 263-278 Automated Reasoning in Kleene Algebra....Pages 279-294 SRASS - A Semantic Relevance Axiom Selection System....Pages 295-310 Labelled Clauses....Pages 311-327 Automatic Decidability and Combinability Revisited....Pages 328-344 Designing Verification Conditions for Software....Pages 345-345 Encodings of Bounded LTL Model Checking in Effectively Propositional Logic....Pages 346-361 Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems....Pages 362-378 The KeY system 1.0 (Deduction Component)....Pages 379-384 KeY-C: A Tool for Verification of C Programs....Pages 385-390 The Bedwyr System for Model Checking over Syntactic Expressions....Pages 391-397 System for Automated Deduction (SAD): A Tool for Proof Verification....Pages 398-403 Logical Engineering with Instance-Based Methods....Pages 404-409 Predictive Labeling with Dependency Pairs Using SAT....Pages 410-425 Dependency Pairs for Rewriting with Non-free Constructors....Pages 426-442 Proving Termination by Bounded Increase....Pages 443-459 Certified Size-Change Termination....Pages 460-475 Encoding First Order Proofs in SAT....Pages 476-491 Hyper Tableaux with Equality....Pages 492-507 System Description: E- KRHyper....Pages 508-513 System Description: Spass Version 3.0....Pages 514-520 Back Matter....Pages - This volume contains the proceedings of the 21st International Conference on AutomatedDeduction, whichwasheldJuly17-20,2007attheJacobsUniversity in Bremen, Germany. CADE is the major forum for the presentation of research in all aspects of automated deduction. There were also a number of a?liated workshops on the days preceding CADE, which helped to make the conference a success. A total of 28 regular papers and 6 system descriptions were selected for presentation from 64 submissions. Each submission was reviewed by at least 4 members of the Program Committee, with the help of 115 external referees. I wouldliketothankallthemembersoftheProgramCommitteefortheirdiligent, careful, and timely work and thoughtful deliberations, and Andrei Voronkov for providing the EasyChair system which greatly facilitated the reviewing p- cess, the electronic Program Committee meeting, and the preparation of the proceedings. In addition to the contributed papers, the program contained four invited talks by Peter Baumgartner, Rustan Leino, Colin Stirling, and Ashish Tiwari. I would like to thank the invited speakers not only for their presentations, but also for contributing abstracts or full papers to the proceedings. During the conference, the 2007 Herbrand Award for Distinguished Cont- butions to Automated Reasoning was given to Alan Bundy in recognition of his outstanding contributions to proof planning and inductive theorem proving, as well as to many other areas of automated reasoning and arti?cial intelligence. ManypeoplehelpedtomakeCADE-21asuccess. Iamparticularlygratefulto MichaelKohlhase(ConferenceChair), ChristophBenzmu ·ller(WorkshopChair), AmyFelty(CADESecretaryandPublicityChair), Geo?Sutcli?e(CASCChair), and all the individual workshop organizers 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.