Automated Deduction – CADE-22: 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings

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 -