| Description |
1 online resource (xv, 466 pages) : illustrations |
| Series |
Lecture notes in computer science, 1611-3349 ; 7898. Lecture notes in artificial intelligence |
|
LNCS sublibrary. SL 7, Artificial intelligence |
|
Lecture notes in computer science ; 7898. 1611-3349
|
|
Lecture notes in computer science. Lecture notes in artificial intelligence
|
|
LNCS sublibrary. SL 7, Artificial intelligence.
|
| Contents |
One Logic to Use Them All / Jean-Christophe Filliâtre -- The Tree Width of Separation Logic with Recursive Definitions / Radu Iosif, Adam Rogalewicz, Jiri Simacek -- Hierarchic Superposition with Weak Abstraction / Peter Baumgartner, Uwe Waldmann -- Completeness and Decidability Results for First-Order Clauses with Indices / Abdelkader Kersani, Nicolas Peltier -- A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies / Marta Cialdea Mayer -- Tractable Inference Systems: An Extension with a Deducibility Predicate / Hubert Comon-Lundh, Véronique Cortier, Guillaume Scerri -- Computing Tiny Clause Normal Forms / Noran Azmy, Christoph Weidenbach -- System Description: E-KRHyper 1.4 / Markus Bender, Björn Pelzer, Claudia Schon -- Analysing Vote Counting Algorithms via Logic / Bernhard Beckert, Rajeev Goré, Carsten Schürmann -- Automated Reasoning, Fast and Slow / Natarajan Shankar -- Foundational Proof Certificates in First-Order Logic / Zakaria Chihani, Dale Miller, Fabien Renaud |
|
Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals / Leonardo de Moura, Grant Olney Passmore -- A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition / Ulrich Loup, Karsten Scheibler, Florian Corzilius -- dReal: An SMT Solver for Nonlinear Theories over the Reals / Sicun Gao, Soonho Kong, Edmund M. Clarke -- Solving Difference Constraints over Modular Arithmetic / Graeme Gange, Harald Søndergaard, Peter J. Stuckey -- Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis / Serdar Erbatur, Santiago Escobar, Deepak Kapur -- Hierarchical Combination / Serdar Erbatur, Deepak Kapur, Andrew M. Marshall -- PRocH: Proof Reconstruction for HOL Light / Cezary Kaliszyk, Josef Urban -- An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description / Rajeev Goré, Jimmy Thomson -- Towards Modularly Comparing Programs Using Automated Theorem Provers / Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri -- Reuse in Software Verification by Abstract Method Calls / Reiner Hähnle, Ina Schaefer, Richard Bubel |
|
Dynamic Logic with Trace Semantics / Bernhard Beckert, Daniel Bruns -- Temporalizing Ontology-Based Data Access / Franz Baader, Stefan Borgwardt, Marcel Lippmann -- Verifying Refutations with Extended Resolution / Marijn J.H. Heule, Warren A. Hunt Jr., Nathan Wetzler -- Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems / Viorica Sofronie-Stokkermans -- Quantifier Instantiation Techniques for Finite Model Finding in SMT / Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstić -- Automating Inductive Proofs Using Theory Exploration / Koen Claessen, Moa Johansson, Dan Rosén -- E-MaLeS 1.1 / Daniel Kühlwein, Stephan Schulz, Josef Urban -- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism / Jasmin Christian Blanchette, Andrei Paskevich -- Propositional Temporal Proving with Reductions to a SAT Problem / Richard Williams, Boris Konev -- InKreSAT: Modal Reasoning via Incremental Reduction to SAT / Mark Kaminski, Tobias Tebbi -- bv2epr: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into EPR / Gergely Kovásznai, Andreas Fröhlich, Armin Biere -- The 481 Ways to Split a Clause and Deal with Propositional Variables / Kryštof Hoder, Andrei Voronkov |
| Summary |
This book constitutes the proceedings of the 24th International Conference on Automated Deduction, CADE-24, held in Lake Placid, NY, USA, in June 2013. The 31 revised full papers presented together with 2 invited papers were carefully reviewed and selected from 71 initial submissions. CADE is the major forum for the presentation of research in all aspects of automated deduction, ranging from theoretical and methodological issues to the presentation of new theorem provers, solvers and systems |
| Analysis |
computerwetenschappen |
|
computer sciences |
|
algoritmen |
|
algorithms |
|
computeranalyse |
|
computer analysis |
|
kunstmatige intelligentie |
|
artificial intelligence |
|
wiskunde |
|
mathematics |
|
logica |
|
logic |
|
software engineering |
|
Information and Communication Technology (General) |
|
Informatie- en communicatietechnologie (algemeen) |
| Bibliography |
Includes bibliographical references and author index |
| Notes |
English |
|
Online resource; title from PDF title page (SpringerLink, viewed July 19, 2013) |
| In |
Springer eBooks |
| Subject |
Automatic theorem proving -- Congresses
|
|
Logic, Symbolic and mathematical -- Congresses
|
|
Logic.
|
|
Mathematics.
|
|
Logic
|
|
Mathematics
|
|
logic.
|
|
Mathematics
|
|
Logic
|
|
Automatic theorem proving
|
|
Logic, Symbolic and mathematical
|
| Genre/Form |
proceedings (reports)
|
|
Conference papers and proceedings
|
|
Conference papers and proceedings.
|
|
Actes de congrès.
|
| Form |
Electronic book
|
| Author |
Bonacina, Maria Paola.
|
| ISBN |
9783642385742 |
|
3642385745 |
|
