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

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 i...

Πλήρης περιγραφή

Λεπτομέρειες βιβλιογραφικής εγγραφής
Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
Άλλοι συγγραφείς: Schmidt, Renate A. (Επιμελητής έκδοσης)
Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
Γλώσσα:English
Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2009.
Σειρά:Lecture Notes in Computer Science, 5663
Θέματα:
Διαθέσιμο Online:Full Text via HEAL-Link
LEADER 05560nam a22005895i 4500
001 978-3-642-02959-2
003 DE-He213
005 20170119000005.0
007 cr nn 008mamaa
008 100301s2009 gw | s |||| 0|eng d
020 |a 9783642029592  |9 978-3-642-02959-2 
024 7 |a 10.1007/978-3-642-02959-2  |2 doi 
040 |d GrThAP 
050 4 |a Q334-342 
050 4 |a TJ210.2-211.495 
072 7 |a UYQ  |2 bicssc 
072 7 |a TJFM1  |2 bicssc 
072 7 |a COM004000  |2 bisacsh 
082 0 4 |a 006.3  |2 23 
245 1 0 |a Automated Deduction – CADE-22  |h [electronic resource] :  |b 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings /  |c edited by Renate A. Schmidt. 
264 1 |a Berlin, Heidelberg :  |b Springer Berlin Heidelberg :  |b Imprint: Springer,  |c 2009. 
300 |a XIV, 504 p.  |b online resource. 
336 |a text  |b txt  |2 rdacontent 
337 |a computer  |b c  |2 rdamedia 
338 |a online resource  |b cr  |2 rdacarrier 
347 |a text file  |b PDF  |2 rda 
490 1 |a Lecture Notes in Computer Science,  |x 0302-9743 ;  |v 5663 
505 0 |a Session 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. 
520 |a 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. 
650 0 |a Computer science. 
650 0 |a Computer programming. 
650 0 |a Software engineering. 
650 0 |a Programming languages (Electronic computers). 
650 0 |a Computer logic. 
650 0 |a Mathematical logic. 
650 0 |a Artificial intelligence. 
650 1 4 |a Computer Science. 
650 2 4 |a Artificial Intelligence (incl. Robotics). 
650 2 4 |a Programming Languages, Compilers, Interpreters. 
650 2 4 |a Programming Techniques. 
650 2 4 |a Mathematical Logic and Formal Languages. 
650 2 4 |a Logics and Meanings of Programs. 
650 2 4 |a Software Engineering. 
700 1 |a Schmidt, Renate A.  |e editor. 
710 2 |a SpringerLink (Online service) 
773 0 |t Springer eBooks 
776 0 8 |i Printed edition:  |z 9783642029585 
830 0 |a Lecture Notes in Computer Science,  |x 0302-9743 ;  |v 5663 
856 4 0 |u http://dx.doi.org/10.1007/978-3-642-02959-2  |z Full Text via HEAL-Link 
912 |a ZDB-2-SCS 
912 |a ZDB-2-LNC 
950 |a Computer Science (Springer-11645)