LEADER 06439nam 22009255 450 001 9910483050003321 005 20251226193450.0 010 $a1-282-33197-3 010 $a9786612331978 010 $a3-642-02959-0 024 7 $a10.1007/978-3-642-02959-2 035 $a(CKB)1000000000761218 035 $a(EBL)451010 035 $a(OCoLC)437346654 035 $a(SSID)ssj0000289523 035 $a(PQKBManifestationID)11260368 035 $a(PQKBTitleCode)TC0000289523 035 $a(PQKBWorkID)10404022 035 $a(PQKB)10839626 035 $a(DE-He213)978-3-642-02959-2 035 $a(MiAaPQ)EBC451010 035 $a(MiAaPQ)EBC6413206 035 $a(PPN)136310664 035 $a(EXLCZ)991000000000761218 100 $a20100301d2009 u| 0 101 0 $aeng 135 $aur|n|---||||| 181 $ctxt 182 $cc 183 $acr 200 10$aAutomated Deduction ? CADE-22 $e22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings /$fedited by Renate Schmidt 205 $a1st ed. 2009. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2009. 215 $a1 online resource (515 p.) 225 1 $aLecture Notes in Artificial Intelligence,$x2945-9141 ;$v5663 300 $aInternational conference proceedings. 311 08$a3-642-02958-2 320 $aIncludes bibliographical references and index. 327 $aSession 1. Invited Talk -- Integrated Reasoning and Proof Choice Point Selection in the Jahob System ? Mechanisms for Program Survival -- Session 2. Combinations and Extensions -- Superposition and Model Evolution Combined -- On Deciding Satisfiability by DPLL( ) and Unsound Theorem Proving -- Combinable Extensions of Abelian Groups -- Locality Results for Certain Extensions of Theories with Bridging Functions -- Session 3. Minimal Unsatisfiability and Automated Reasoning Support -- Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis -- Does This Set of Clauses Overlap with at Least One MUS? -- Progress in the Development of Automated Theorem Proving for Higher-Order Logic -- Session 4. System Descriptions -- System Description: H-PILoT -- SPASS Version 3.5 -- Dei: A Theorem Prover for Terms with Integer Exponents -- veriT: An Open, Trustable and Efficient SMT-Solver -- Divvy: An ATP Meta-system Based on Axiom Relevance Ordering -- Session 5. Invited Talk -- Instantiation-Based Automated Reasoning: From Theory to Practice -- Session 6. Interpolation and Predicate Abstraction -- Interpolant Generation for UTVPI -- Ground Interpolation for Combined Theories -- Interpolation and Symbol Elimination -- Complexity and Algorithms for Monomial and Clausal Predicate Abstraction -- Session 7. Resolution-Based Systems for Non-classical Logics -- Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method -- A Refined Resolution Calculus for CTL -- Fair Derivations in Monodic Temporal Reasoning -- Session 8. Termination Analysis and Constraint Solving -- A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs -- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic -- Session 9. Invited Talk.-Building Theorem Provers -- Session 10. Rewriting, Termination and Productivity -- Termination Analysis by Dependency Pairs and Inductive Theorem Proving -- Beyond Dependency Graphs -- Computing Knowledge in Security Protocols under Convergent Equational Theories -- Complexity of Fractran and Productivity -- Session 11. Models -- Automated Inference of Finite Unsatisfiability -- Decidability Results for Saturation-Based Model Building -- Session 12. Modal Tableaux with Global Caching -- A Tableau Calculus for Regular Grammar Logics with Converse -- An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability -- Session 13. Arithmetic -- Volume Computation for Boolean Combination of Linear Arithmetic Constraints -- A Generalization of Semenov?s Theorem to Automata over Real Numbers -- Real World Verification. 330 $aThis 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. 410 0$aLecture Notes in Artificial Intelligence,$x2945-9141 ;$v5663 606 $aArtificial intelligence 606 $aCompilers (Computer programs) 606 $aComputer programming 606 $aMachine theory 606 $aComputer science 606 $aSoftware engineering 606 $aArtificial Intelligence 606 $aCompilers and Interpreters 606 $aProgramming Techniques 606 $aFormal Languages and Automata Theory 606 $aComputer Science Logic and Foundations of Programming 606 $aSoftware Engineering 615 0$aArtificial intelligence. 615 0$aCompilers (Computer programs). 615 0$aComputer programming. 615 0$aMachine theory. 615 0$aComputer science. 615 0$aSoftware engineering. 615 14$aArtificial Intelligence. 615 24$aCompilers and Interpreters. 615 24$aProgramming Techniques. 615 24$aFormal Languages and Automata Theory. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aSoftware Engineering. 676 $a006.3 686 $aDAT 706f$2stub 686 $aDAT 716f$2stub 686 $aSS 4800$2rvk 686 $a004$2sdnb 686 $a510$2sdnb 702 $aSchmidt$b Renate A. 712 12$aInternational Conference on Automated Deduction 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910483050003321 996 $aAutomated deduction - CADE-22$92812254 997 $aUNINA