Conference proceedings of the International Conference on Automated Deduction, CADE-24, 2013

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.