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 Cover ......Page 1 Automated Deduction – CADE-22 - 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009, Proceedings ......Page 3 ISBN-10 3642029582 ISBN-13 9783642029585......Page 4 Preface......Page 6 Conference Organization......Page 8 Table of Contents......Page 12 Integrated Reasoning and Proof Choice Point Selection in the Jahob System – Mechanisms for Program Survival......Page 16 Integrated Reasoning......Page 17 Program Survival......Page 19 Static Verification of Survival Properties......Page 20 Failure-Oblivious Computing......Page 21 Loop Termination......Page 22 Data Structure Consistency......Page 23 The Jahob Specification Language......Page 24 The Jahob Integrated Proof Language......Page 25 Hob......Page 26 Infinite Loops......Page 27 Memory Leaks......Page 28 Conclusion......Page 29 Introduction......Page 32 Formal Preliminaries......Page 34 Contexts......Page 36 Constrained Clauses......Page 37 Inference Rules on Constrained Clauses......Page 38 Inference Rules on Sequents......Page 40 Model Construction......Page 42 Redundancy, Saturation and Static Completeness......Page 44 Derivations with Simplification......Page 46 Conclusions......Page 48 Introduction......Page 50 Background......Page 52 Variable Inactivity in DPLL($\Gamma+\T$)......Page 53 Unsound Theorem Proving in DPLL($\Gamma+\T$)......Page 54 Essentially Finite Theories......Page 59 Discussion......Page 63 Introduction......Page 66 Preliminaries......Page 67 A Brief Overview on Non-disjoint Combination......Page 68 The Theory of Abelian Groups......Page 69 Noetherianity of Abelian Groups......Page 70 An Extension of Abelian Groups Having Quantifier Elimination......Page 71 A Calculus for Abelian Groups......Page 72 Refutational Completeness of ${\mathcal SP}_{AG}$}......Page 74 Computing AG-Bases......Page 76 Some Examples......Page 77 Applying the Combination Framework......Page 78 Conclusion......Page 79 Introduction......Page 82 Preliminaries......Page 83 Functions on Absolutely Free Data Structures......Page 86 A Class of Recursively Defined Functions......Page 87 Restricting to Term-Generated Algebras......Page 91 More General Data Structures......Page 93 An Example Inspired from Cryptography......Page 95 Conclusion......Page 96 Motivations and Goals......Page 99 Classification, Subsumption and Axiom Pinpointing in ${\mathcal{EL^{+}}}$......Page 100 Basics on Conflict-Driven SAT Solving......Page 103 Classification and Concept Subsumption via Horn SAT Solving......Page 105 Computing Single and All MinAs via Conflict Analysis......Page 106 Discussion......Page 110 Empirical Evaluation......Page 111 Ongoing and Future Work......Page 113 Introduction......Page 115 Logical Preliminaries, MUSes and Shapley’s Measure......Page 116 MUSes of a SAT Instance......Page 117 Main Principles Underlying the Approach......Page 118 FromMUSes toMUSCes......Page 119 Initiating the Process......Page 122 Iterating and Ending the Process......Page 123 Main Algorithm......Page 125 Experimental Results......Page 127 Other RelevantWorks......Page 128 References......Page 129 Motivation and History......Page 131 The Typed Higher-Order Form (THF) Language......Page 132 Collecting THF Problems, for the TPTP......Page 135 Collecting Solutions to THF Problems, for the TSTP......Page 137 LEO-II......Page 138 Tps......Page 139 IsabelleP and IsabelleM......Page 140 Cunning Plans for the Future......Page 141 Conclusion......Page 142 Introduction......Page 146 Theoretical Background......Page 147 Preprocessing......Page 148 Main Algorithm......Page 149 System Evaluation......Page 150 Test Runs for H-PILoT......Page 151 Test Results......Page 152 Introduction......Page 155 Subterm Contextual Rewriting......Page 156 Further Enhancements......Page 158 Future Work......Page 159 Introduction......Page 161 TheDei System......Page 162 Inferences......Page 163 A Short Example......Page 164 References......Page 165 Introduction......Page 166 Integrating a First-Order Prover......Page 167 Proofs......Page 168 Future Work......Page 170 Motivation, History, and Overview......Page 172 Ordering Based on Latent Semantic Analysis......Page 173 The Divvy ATP Meta-system......Page 174 Evaluation......Page 175 Conclusion......Page 177 Instantiation-Based Automated Reasoning: From Theory to Practice......Page 178 References......Page 180 Motivations and Goals......Page 182 Background......Page 184 Graph-Based Interpolation for ${\ensuremath{\mathcal{UTVPI(\mathbb{Z})}}$......Page 186 Graph-Based Interpolation for ${\ensuremath{\mathcal{UTVPI(\mathbb{Q})}}$......Page 188 Experimental Evaluation......Page 194 Conclusions......Page 196 Introduction......Page 198 Resolution Proof Trees......Page 200 Theories......Page 201 Modifying Proof Trees......Page 202 Prelude......Page 203 The Colorability Theorem......Page 205 The Colorability Algorithm......Page 207 Almost-Colorable Refutations from SMT Solvers......Page 209 Conclusion......Page 212 Introduction......Page 214 Preliminaries......Page 215 Inference Systems and Local Derivation......Page 217 Superposition and Interpolation......Page 223 Interpolation and Invariant Generation......Page 225 Related Work......Page 226 Conclusion......Page 227 Introduction......Page 229 A Simple Programming Language for Loop-Free Programs......Page 231 Complexity of Predicate and Template Abstraction......Page 233 Predicate Abstraction......Page 234 Monomial Abstraction......Page 235 Houdini Algorithm......Page 236 Symbolic Encoding and Complexity of InferMonome(Prog, ${\mathcal P}$)......Page 237 Dual Houdini Algorithm......Page 239 Model-Theoretic Proof......Page 240 Conclusions......Page 241 Introduction......Page 245 Polarized Formulas......Page 246 Backward Polarized Sequent Calculus......Page 247 Synthetic Connectives and Derived Rules......Page 249 Forward Rules......Page 250 Proof Search......Page 252 An Implementation Framework......Page 253 The Back End: Rule Application and Subsumption......Page 254 Subsumption......Page 255 Performance Evaluation......Page 256 Conclusion......Page 258 Introduction......Page 260 Syntax and Semantics of CTL......Page 261 Normal Form......Page 262 The Clausal Resolution Calculus $\Rctl$......Page 263 Properties of $\Rctl$......Page 266 Implementation and Experiments......Page 272 Related Work and Conclusions......Page 274 Introduction......Page 276 First-Order Temporal Logic......Page 277 Ordered Fine-Grained Resolution with Selection......Page 280 Constructing Fair Derivations......Page 283 Refutational Completeness......Page 287 Implementation......Page 289 Conclusion......Page 291 Introduction......Page 292 ${\mathcal PA}$-Based TRSs......Page 294 Translating Imperative Programs into ${\mathcal PA}$-Based TRSs......Page 295 Characterizing Termination of ${\mathcal PA}$-Based TRSs......Page 297 Termination Graphs......Page 298 ${\mathcal PA}$-Polynomial Interpretations......Page 299 Chaining......Page 300 Generation of ${\mathcal PA}$-Polynomial Interpretations......Page 301 Conclusions and Future Work......Page 305 References......Page 306 Introduction......Page 309 Integer Intervals......Page 311 Finite Rational Domains......Page 313 Choosing Variables for Simplification......Page 314 Choosing Domains......Page 315 Experiments Using MU-TERM......Page 316 Experiments Using AProVE......Page 317 Conclusions......Page 318 The British Museum Algorithm Reconsidered......Page 321 Pttp, Another Simple Complete Theorem Prover......Page 324 Building Applications with Theorem Provers......Page 325 Deductive Question Answering......Page 326 Goal-Orientedness, an Elusive Goal......Page 327 Procedural Attachment, Get Someone Else to Do It......Page 328 Sorts, Hybrid Reasoning Made Easy......Page 330 AC Unification, the Long Road to Full Use......Page 332 Conclusion......Page 333 Introduction......Page 337 Dependency Pairs......Page 339 Many-Sorted Rewriting......Page 342 Coupling DPs and Inductive Theorem Proving......Page 345 Experiments and Conclusion......Page 351 Introduction......Page 354 Preliminaries......Page 355 Tree Automata Completion......Page 356 Incorporating Forward Closures......Page 358 Comparison......Page 362 Innermost Termination......Page 364 Experimental Results......Page 365 Introduction......Page 370 Equational Theories and Rewriting Systems......Page 372 Deducibility and Static Equivalence......Page 373 Preliminary Definitions......Page 374 Saturation Procedure......Page 375 Application to Deduction and Static Equivalence......Page 378 Soundness and Completeness......Page 379 Generic Method for Proving Termination......Page 380 Applications......Page 381 Implementation......Page 383 Conclusion......Page 384 Introduction......Page 386 Fractran......Page 390 What Is Productivity?......Page 394 Productivity with Respect to Strategies......Page 395 Strong Productivity......Page 397 Weak Productivity......Page 398 Discussion......Page 399 Productivity for Lazy Stream Specifications Is $\cpi{0}{2}$}......Page 400 Introduction......Page 403 Generalizing Equality to Reflexive Relations......Page 405 Functions That Are Surjective and Not Injective......Page 406 Relations That Are Irreflexive, Transitive and Serial......Page 407 Summing Up......Page 408 The Main Architecture......Page 409 Enumerating Functions and Relations......Page 410 Filtering......Page 411 Results......Page 412 Comparisons......Page 413 Conclusions......Page 416 Introduction......Page 419 Preliminaries......Page 421 A Constrained Ordered Resolution Calculus......Page 423 Decidability of Model Equivalence and Formula Entailment for DIGs......Page 427 Conclusion......Page 433 Introduction......Page 436 Regular Semi-thue Systems......Page 438 Regular Grammar Logics with Converse......Page 439 A Tableau Calculus for ${REG}^c$......Page 440 Proof of Completeness......Page 444 The Basic Algorithm......Page 447 Optimizations......Page 449 Conclusions......Page 450 Introduction......Page 452 Syntax and Semantics......Page 453 An Overview and Our Algorithm......Page 455 The Algorithm......Page 457 A Fully Worked Example......Page 464 Implementation Issues and Experiments......Page 466 Introduction......Page 468 Background......Page 469 A Straightforward Method......Page 470 The Basic Idea......Page 471 The Algorithm......Page 473 Incorporating Theory-Level Conflict-Driven Learning......Page 475 Implementation and Experimental Results......Page 476 Application to Program Analysis......Page 477 Execution Probability......Page 478 A Practical Example......Page 479 Related Works and Discussion......Page 480 Concluding Remarks......Page 481 A Generalization of Semenov's Theorem to Automata over Real Numbers......Page 484 Introduction......Page 485 Real Vector Automata......Page 487 Properties of Recognizable Sets......Page 488 Reduction to Product-Stable Sets......Page 490 Using s-Recognizability......Page 492 Exploiting Multiple Product Stabilities......Page 493 Internal Structure of RVA......Page 495 Conclusions......Page 497 Introduction......Page 500 Gröbner Bases for Real Arithmetic......Page 502 A Complete Rule Using the Real Nullstellensatz......Page 505 Quantifier Elimination in Real-Closed Fields......Page 506 Semidefinite Programming for the Positivstellensatz......Page 507 Gröbner Bases for the Real Nullstellensatz (GRN)......Page 508 Discussion and Practical Considerations......Page 510 Experimental Results......Page 511 Related Work......Page 512 Discussion and Conclusions......Page 513 Author Index......Page 518