Automated Deduction - Cade-22

by Schmidt, Renate A.

• ISBN13: 9783642029585
• ISBN10: 3642029582
• Format: Paperback
• Copyright: 2009-08-01
• Publisher: Springer-Verlag New York Inc

Summary

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.

Table of Contents

Invited Talk
Integrated Reasoning and Proof Choice Point Selection in the Jahob System - Mechanisms for Program Survival	p. 1
Combinations and Extensions
Superposition and Model Evolution Combined	p. 17
On Deciding Satisfiability by DPLL(¿ + T) and Unsound Theorem Proving	p. 35
Combinable Extensions of Abelian Groups	p. 51
Locality Results for Certain Extensions of Theories with Bridging Functions	p. 67
Minimal Unsatisfiability and Automated Reasoning Support
Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis	p. 84
Does This Set of Clauses Overlap with at Least One MUS?	p. 100
Progress in the Development of Automated Theorem Proving for Higher-Order Logic	p. 116
System Descriptions
System Description: H-PILoT	p. 131
SPASS Version 3.5	p. 140
Dei: A Theorem Prover for Terms with Integer Exponents	p. 146
veriT: An Open, Trustable and Efficient SMT-Solver	p. 151
Divvy: An ATP Meta-system Based on Axiom Relevance Ordering	p. 157
Invited Talk
Instantiation-Based Automated Reasoning: From Theory to Practice	p. 163
Interpolation and Predicate Abstraction Interpolant Generation for UTVPI	p. 167
Ground Interpolation for Combined Theories	p. 183
Interpolation and Symbol Elimination	p. 199
Complexity and Algorithms for Monomial and Clausal Predicate Abstraction	p. 214
Resolution-Based Systems for Non-classical Logics
Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method	p. 230
A Refined Resolution Calculus for CTL	p. 245
Fair Derivations in Monodic Temporal Reasoning	p. 261
Termination Analysis and Constraint Solving
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs	p. 277
Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic	p. 294
Invited Talk
Building Theorem Provers	p. 306
Rewriting, Termination and Productivity
Termination Analysis by Dependency Pairs and Inductive Theorem Proving	p. 322
Beyond Dependency Graphs	p. 339
Computing Knowledge in Security Protocols under Convergent Equational Theories	p. 355
Complexity of Fractran and Productivity	p. 371
Models
Automated Inference of Finite Unsatisfiability	p. 388
Decidability Results for Saturation-Based Model Building	p. 404
Modal Tableaux with Global Caching
A Tableau Calculus for Regular Grammar Logics with Converse	p. 421
An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability	p. 421
Arithmetic
Volume Computation for Boolean Combination of Linear Arithmetic Constraints	p. 453
A Generalization of Semenov's Theorem to Automata over Real Numbers	p. 469
Real World Verification	p. 485
Author Index	p. 503
Table of Contents provided by Ingram. All Rights Reserved.