Automated Deduction  CADE-24 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings /

• Corporate Author: SpringerLink (Online service)
• Other Authors: Bonacina, Maria Paola. (Editor)
• Format: Electronic
• Language: English
• Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2013.
• Series: Lecture Notes in Computer Science, 7898
• Subjects: Computer science.; Software engineering.; Computer software.; Logic design.; Artificial intelligence.; Computer Science.; Artificial Intelligence (incl. Robotics).; Mathematical Logic and Formal Languages.; Logics and Meanings of Programs.; Software Engineering.; Algorithm Analysis and Problem Complexity.
• Online Access: https://ezaccess.library.uitm.edu.my/login?url=http://dx.doi.org/10.1007/978-3-642-38574-2

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

Table of Contents:

• One Logic to Use Them All
• The Tree Width of Separation Logic with Recursive Definitions
• Hierarchic Superposition with Weak Abstraction
• Completeness and Decidability Results for First-Order Clauses with Indices
• A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies
• Tractable Inference Systems: An Extension with a Deducibility Predicate
• Computing Tiny Clause Normal Forms
• System Description: E-KRHyper 1.4 Extensions for Unique Names and Description Logic
• Analysing Vote Counting Algorithms via Logic: And Its Application to the CADE Election Scheme
• Automated Reasoning, Fast and Slow
• Foundational Proof Certificates in First-Order Logic
• Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
• A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition
• dReal: An SMT Solver for Nonlinear Theories over the Reals
• Solving Difference Constraints over Modular Arithmetic
• Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis
• Hierarchical Combination
• PRocH: Proof Reconstruction for HOL Light
• An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description
• Towards Modularly Comparing Programs Using Automated Theorem Provers
• Reuse in Software Verification by Abstract Method Calls
• Dynamic Logic with Trace Semantics
• Temporalizing Ontology-Based Data Access
• Verifying Refutations with Extended Resolution
• Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems
• Quantifier Instantiation Techniques for Finite Model Finding in SMT
• Automating Inductive Proofs Using Theory Exploration
• E-MaLeS 1.1
• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
• Propositional Temporal Proving with Reductions to a SAT Problem
• InKreSAT: Modal Reasoning via Incremental Reduction to SAT
• bv2epr: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into EPR
• The 481 Ways to Split a Clause and Deal with Propositional Variables.