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.
Author(s): Colin Stirling (auth.), Frank Pfenning (eds.)
Series: Lecture Notes in Computer Science 4603
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2007
Language: English
Pages: 524
Tags: Artificial Intelligence (incl. Robotics); Mathematical Logic and Formal Languages; Logics and Meanings of Programs; Software Engineering
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 -
