Automated Deduction -- CADE 21

by Pfenning, Frank

• ISBN13: 9783540735946
• ISBN10: 3540735941
• Format: Paperback
• Copyright: 2007-09-03
• Publisher: Springer-Verlag New York Inc

Summary

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 Matching	p. 1
Higher-Order Logic
Formalization of Continuous Probability Distributions	p. 3
Compilation as Rewriting in Higher Order Logic	p. 19
Barendregt's Variable Convention in Rule Inductions	p. 35
Automating Elementary Number-Theoretic Proofs Using Grobner Bases	p. 51
Description Logic
Optimized Reasoning in Description Logics Using Hypertableaux	p. 67
Conservative Extensions in the Lightweight Description Logic EL	p. 84
An Incremental Technique for Automata-Based Decision Procedures	p. 100
Intuitionistic Logic
Bidirectional Decision Procedures for the Intuitionistic Prepositional Modal Logic IS4	p. 116
A Labelled System for IPL with Variable Splitting	p. 132
Invited Talk: Ashish Tiwari
Logical Interpretation: Static Program Analysis Using Theorem Proving	p. 147
Satisfiability Modulo Theories
Solving Quantified Verification Conditions Using Satisfiability Modulo Theories	p. 167
Efficient E-Matching for SMT Solvers	p. 183
T-Decision by Decomposition	p. 199
Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic	p. 215
Induction, Rewriting, and Polymorphism
Improvements in Formula Generalization	p. 231
On the Normalization and Unique Normalization Properties of Term Rewrite Systems	p. 247
Handling Polymorphism in Automated Deduction	p. 263
First-Order Logic
Automated Reasoning in Kleene Algebra	p. 279
SRASS - A Semantic Relevance Axiom Selection System	p. 295
Labelled Clauses	p. 311
Automatic Decidability and Combinability Revisited	p. 328
Invited Talk: K. Rustan M. Leino
Designing Verification Conditions for Software	p. 345
Model Checking and Verification
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic	p. 346
Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems	p. 362
The KeY System 1.0	p. 379
KeY-C: A Tool for Verification of C Programs	p. 385
The Bedwyr System for Model Checking over Syntactic Expressions	p. 391
System for Automated Deduction (SAD): A Tool for Proof Verification	p. 398
Invited Talk: Peter Baumgartner
Logical Engineering with Instance-Based Methods	p. 404
Termination
Predictive Labeling with Dependency Pairs Using SAT	p. 410
Dependency Pairs for Rewriting with Non-free Constructors	p. 426
Proving Termination by Bounded Increase	p. 443
Certified Size-Change Termination	p. 460
Tableaux and First-Order Systems
Encoding First Order Proofs in SAT	p. 476
Hyper Tableaux with Equality	p. 492
System Description: E-KRHyper	p. 508
System Description: SPASS Version 3.0	p. 514
Author Index	p. 521
Table of Contents provided by Ingram. All Rights Reserved.