Automated Deduction – Cade-22: 22nd International Conference On Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings (lecture Notes In Computer Science)

Annotation This book constitutes the refereed proceedings of the 22nd International Conference on Automated Deduction, CADE-22, held in Montreal, Canada, in August 2009. The 27 revised full papers and 5 system descriptions presented were carefully reviewed and selected from 77 submissions. Furthermore, three invited lectures by distinguished experts in the area were included. The papers are organized in topical sections on combinations and extensions, minimal unsatisfiability and automated reasoning support, system descriptions, interpolation and predicate abstraction, resolution-based systems for non-classical logics, termination analysis and constraint solving, rewriting, termination and productivity, models, modal tableaux with global caching, arithmetic Front Matter....Pages - Integrated Reasoning and Proof Choice Point Selection in the Jahob System – Mechanisms for Program Survival....Pages 1-16 Superposition and Model Evolution Combined....Pages 17-34 On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving....Pages 35-50 Combinable Extensions of Abelian Groups....Pages 51-66 Locality Results for Certain Extensions of Theories with Bridging Functions....Pages 67-83 Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis....Pages 84-99 Does This Set of Clauses Overlap with at Least One MUS?....Pages 100-115 Progress in the Development of Automated Theorem Proving for Higher-Order Logic....Pages 116-130 System Description: H-PILoT....Pages 131-139 SPASS Version 3.5....Pages 140-145 Dei : A Theorem Prover for Terms with Integer Exponents....Pages 146-150 veriT : An Open, Trustable and Efficient SMT-Solver....Pages 151-156 Divvy : An ATP Meta-system Based on Axiom Relevance Ordering....Pages 157-162 Instantiation-Based Automated Reasoning: From Theory to Practice....Pages 163-166 Interpolant Generation for UTVPI....Pages 167-182 Ground Interpolation for Combined Theories....Pages 183-198 Interpolation and Symbol Elimination....Pages 199-213 Complexity and Algorithms for Monomial and Clausal Predicate Abstraction....Pages 214-229 Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method....Pages 230-244 A Refined Resolution Calculus for CTL....Pages 245-260 Fair Derivations in Monodic Temporal Reasoning....Pages 261-276 A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs....Pages 277-293 Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic....Pages 294-305 Building Theorem Provers....Pages 306-321 Termination Analysis by Dependency Pairs and Inductive Theorem Proving....Pages 322-338 Beyond Dependency Graphs....Pages 339-354 Computing Knowledge in Security Protocols under Convergent Equational Theories....Pages 355-370 Complexity of Fractran and Productivity....Pages 371-387 Automated Inference of Finite Unsatisfiability....Pages 388-403 Decidability Results for Saturation-Based Model Building....Pages 404-420 A Tableau Calculus for Regular Grammar Logics with Converse....Pages 421-436 An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability....Pages 437-452 Volume Computation for Boolean Combination of Linear Arithmetic Constraints....Pages 453-468 A Generalization of Semenov’s Theorem to Automata over Real Numbers....Pages 469-484 Real World Verification....Pages 485-501 Back Matter....Pages -