Coverart for item
The Resource Automated deduction - CADE-22 : 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009 ; proceedings, Renate A. Schmidt (ed.)

Automated deduction - CADE-22 : 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009 ; proceedings, Renate A. Schmidt (ed.)

Label
Automated deduction - CADE-22 : 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009 ; proceedings
Title
Automated deduction - CADE-22
Title remainder
22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009 ; proceedings
Statement of responsibility
Renate A. Schmidt (ed.)
Title variation
CADE-22
Creator
Contributor
Subject
Genre
Language
eng
Summary
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
Member of
Cataloging source
GW5XE
Dewey number
006.3/33
Illustrations
illustrations
Index
no index present
LC call number
QA76.9.A96
LC item number
I58 2009
Literary form
non fiction
http://bibfra.me/vocab/lite/meetingDate
2009
http://bibfra.me/vocab/lite/meetingName
International Conference on Automated Deduction
Nature of contents
  • dictionaries
  • bibliography
NLM call number
QA 76.9.A96
http://library.link/vocab/relatedWorkOrContributorName
Schmidt, Renate A
Series statement
  • Lecture notes in computer science,
  • Lecture notes in artificial intelligence
Series volume
5663
http://library.link/vocab/subjectName
  • Automatic theorem proving
  • Logic machines
  • Computing Methodologies
  • Logic
  • Automatic theorem proving
  • Logic machines
  • Informatique
  • Automatic theorem proving
  • Logic machines
  • Automatisches Beweisverfahren
Label
Automated deduction - CADE-22 : 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009 ; proceedings, Renate A. Schmidt (ed.)
Instantiates
Publication
Note
International conference proceedings
Bibliography note
Includes bibliographical references
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
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
Control code
437346654
Dimensions
unknown
Extent
1 online resource (xiv, 504 pages)
Form of item
online
Isbn
9783642029592
Lccn
2015458534
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
  • 9786612331978
  • 9783642029585
  • 10.1007/978-3-642-02959-2
Other physical details
illustrations.
http://library.link/vocab/ext/overdrive/overdriveId
978-3-642-02958-5
Publisher number
12717996
Specific material designation
remote
System control number
(OCoLC)437346654
Label
Automated deduction - CADE-22 : 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009 ; proceedings, Renate A. Schmidt (ed.)
Publication
Note
International conference proceedings
Bibliography note
Includes bibliographical references
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Color
multicolored
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
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
Control code
437346654
Dimensions
unknown
Extent
1 online resource (xiv, 504 pages)
Form of item
online
Isbn
9783642029592
Lccn
2015458534
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Other control number
  • 9786612331978
  • 9783642029585
  • 10.1007/978-3-642-02959-2
Other physical details
illustrations.
http://library.link/vocab/ext/overdrive/overdriveId
978-3-642-02958-5
Publisher number
12717996
Specific material designation
remote
System control number
(OCoLC)437346654

Library Locations

    • Ellis LibraryBorrow it
      1020 Lowry Street, Columbia, MO, 65201, US
      38.944491 -92.326012
    • Engineering Library & Technology CommonsBorrow it
      W2001 Lafferre Hall, Columbia, MO, 65211, US
      38.946102 -92.330125
Processing Feedback ...