Automated Deduction -- CADE-24

1. Front Matter

   PDF

2. One Logic to Use Them All

   • Jean-Christophe Filliâtre

   Pages 1-20

3. The Tree Width of Separation Logic with Recursive Definitions

   • Radu Iosif, Adam Rogalewicz, Jiri Simacek

   Pages 21-38

4. Hierarchic Superposition with Weak Abstraction

   • Peter Baumgartner, Uwe Waldmann

   Pages 39-57

5. Completeness and Decidability Results for First-Order Clauses with Indices

   • Abdelkader Kersani, Nicolas Peltier

   Pages 58-75

6. A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies

   • Marta Cialdea Mayer

   Pages 76-90

7. Tractable Inference Systems: An Extension with a Deducibility Predicate

   • Hubert Comon-Lundh, Véronique Cortier, Guillaume Scerri

   Pages 91-108

8. Computing Tiny Clause Normal Forms

   • Noran Azmy, Christoph Weidenbach

   Pages 109-125

9. System Description: E-KRHyper 1.4

   • Markus Bender, Björn Pelzer, Claudia Schon

   Pages 126-134

10. Analysing Vote Counting Algorithms via Logic

    • Bernhard Beckert, Rajeev Goré, Carsten Schürmann

    Pages 135-144

11. Automated Reasoning, Fast and Slow

    • Natarajan Shankar

    Pages 145-161

12. Foundational Proof Certificates in First-Order Logic

    • Zakaria Chihani, Dale Miller, Fabien Renaud

    Pages 162-177

13. Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals

    • Leonardo de Moura, Grant Olney Passmore

    Pages 178-192

14. A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition

    • Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Ábrahám, Bernd Becker

    Pages 193-207

15. dReal: An SMT Solver for Nonlinear Theories over the Reals

    • Sicun Gao, Soonho Kong, Edmund M. Clarke

    Pages 208-214

16. Solving Difference Constraints over Modular Arithmetic

    • Graeme Gange, Harald Søndergaard, Peter J. Stuckey, Peter Schachte

    Pages 215-230

17. Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis

    • Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher A. Lynch, Catherine Meadows et al.

    Pages 231-248

18. Hierarchical Combination

    • Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, Paliath Narendran, Christophe Ringeissen

    Pages 249-266

19. PRocH: Proof Reconstruction for HOL Light

    • Cezary Kaliszyk, Josef Urban

    Pages 267-274

20. An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description

    • Rajeev Goré, Jimmy Thomson

    Pages 275-281

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.

• AI logics
• difference constraints
• finite models
• hybrid logic
• model checking
• software verification
• algorithm analysis and problem complexity

• Dipartimento di Informatica, Università degli Studi di Verona, Verona, Italy

  Maria Paola Bonacina

Policies and ethics