Automated Deduction -- CADE-23

1. Front Matter

   PDF

2. The Anatomy of Equinox – An Extensible Automated Reasoning Tool for First-Order Logic and Beyond

   • Koen Claessen

   Pages 1-3

3. Advances in Proving Program Termination and Liveness

   • Byron Cook

   Pages 4-4

4. Translating between Language and Logic: What Is Easy and What Is Difficult

   • Aarne Ranta

   Pages 5-25

5. ASASP: Automated Symbolic Analysis of Security Policies

   • Francesco Alberti, Alessandro Armando, Silvio Ranise

   Pages 26-33

6. Backward Trace Slicing for Rewriting Logic Theories

   • María Alpuente, Demis Ballis, Javier Espert, Daniel Romero

   Pages 34-48

7. Deciding Security for Protocols with Recursive Tests

   • Mathilde Arnaud, Véronique Cortier, Stéphanie Delaune

   Pages 49-63

8. The Matita Interactive Theorem Prover

   • Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi

   Pages 64-69

9. Unification in the Description Logic \(\mathcal{EL}\) without the Top Concept

   • Franz Baader, Nguyen Thanh Binh, Stefan Borgwardt, Barbara Morawska

   Pages 70-84

10. Model Evolution with Equality Modulo Built-in Theories

    • Peter Baumgartner, Cesare Tinelli

    Pages 85-100

11. Blocked Clause Elimination for QBF

    • Armin Biere, Florian Lonsing, Martina Seidl

    Pages 101-115

12. Extending Sledgehammer with SMT Solvers

    • Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson

    Pages 116-130

13. Automated Cyclic Entailment Proofs in Separation Logic

    • James Brotherston, Dino Distefano, Rasmus Lerchedahl Petersen

    Pages 131-146

14. Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems

    • Chad E. Brown

    Pages 147-161

15. Experimenting with Deduction Modulo

    • Guillaume Burel

    Pages 162-176

16. Heaps and Data Structures: A Challenge for Automated Provers

    • Sascha Böhme, Michał Moskal

    Pages 177-191

17. Optimized Query Rewriting for OWL 2 QL

    • Alexandros Chortaras, Despoina Trivela, Giorgos Stamou

    Pages 192-206

18. Sort It Out with Monotonicity

    • Koen Claessen, Ann Lillieström, Nicholas Smallbone

    Pages 207-221

19. Exploiting Symmetry in SMT Problems

    • David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo

    Pages 222-236

20. Compression of Propositional Resolution Proofs via Partial Regularization

    • Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo

    Pages 237-251

This book constitutes the refereed proceedings of the 23rd International Conference on Automated Deduction, CADE-23, held in Wrocław, Poland, in July/August 2011.
The 28 revised full papers and 7 system descriptions presented were carefully reviewed and selected from 80 submissions. Furthermore, four invited lectures by distinguished experts in the area were included. Among the topics addressed are systems and tools for automated reasoning, rewriting logics, security protocol verification, unification, theorem proving, clause elimination, SAT, satifiability, interactive theorem proving, theory reasoning, static analysis, decision procedures, etc.

• AI logics
• computer aided verification
• formal methods
• logical reasoning
• model-based program analysis
• term rewriting systems
• termination

• Microsoft Research, Redmond, USA

  Nikolaj Bjørner

• Max-Planck-Institut für Informatik, Saarbrücken, Germany

  Viorica Sofronie-Stokkermans

Policies and ethics