23. CADE 2011: Wroclaw, Poland
Nikolaj Bjørner, Viorica Sofronie-Stokkermans (Eds.): Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings. Springer 2011 Lecture Notes in Computer Science ISBN 978-3-642-22437-9- Koen Claessen: The Anatomy of Equinox - An Extensible Automated Reasoning Tool for First-Order Logic and Beyond - (Talk Abstract). 1-3
- Byron Cook: Advances in Proving Program Termination and Liveness. 4
- Aarne Ranta: Translating between Language and Logic: What Is Easy and What Is Difficult. 5-25
- Francesco Alberti, Alessandro Armando, Silvio Ranise: ASASP: Automated Symbolic Analysis of Security Policies. 26-33
- María Alpuente, Demis Ballis, Javier Espert, Daniel Romero: Backward Trace Slicing for Rewriting Logic Theories. 34-48
- Mathilde Arnaud, Véronique Cortier, Stéphanie Delaune: Deciding Security for Protocols with Recursive Tests. 49-63
- Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi: The Matita Interactive Theorem Prover. 64-69
- Franz Baader, Thanh Binh Nguyen, Stefan Borgwardt, Barbara Morawska: Unification in the Description Logic EL without the Top Concept. 70-84
- Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson: Extending Sledgehammer with SMT Solvers. 116-130
- James Brotherston, Dino Distefano, Rasmus Lerchedahl Petersen: Automated Cyclic Entailment Proofs in Separation Logic. 131-146
- Chad E. Brown: Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems. 147-161
- Guillaume Burel: Experimenting with Deduction Modulo. 162-176
- Alexandros Chortaras, Despoina Trivela, Giorgos B. Stamou: Optimized Query Rewriting for OWL 2 QL. 192-206
- Koen Claessen, Ann Lillieström, Nicholas Smallbone: Sort It Out with Monotonicity - Translating between Many-Sorted and Unsorted First-Order Logic. 207-221
- David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo: Exploiting Symmetry in SMT Problems. 222-236
- Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo: Compression of Propositional Resolution Proofs via Partial Regularization. 237-251
- Matthew Fredrikson, Mihai Christodorescu, Somesh Jha: Dynamic Behavior Matching: A Complexity Analysis and New Approximation Algorithms. 252-267
- Didier Galmiche, Daniel Méry: A Connection-Based Characterization of Bi-intuitionistic Validity. 268-282
- Volker Haarslev, Roberto Sebastiani, Michele Vescovi: Automated Reasoning in ALCQ\mathcal{ALCQ} via SMT. 283-298
- Matthias Horbach: Predicate Completion for non-Horn Clause Sets. 315-330
- Matthias Horbach: System Description: SPASS-FD. 331-337
- Dejan Jovanovic, Leonardo Mendonça de Moura: Cutting to the Chase Solving Linear Integer Arithmetic. 338-353
- Konstantin Korovin, Andrei Voronkov: Solving Systems of Linear Inequalities by Bound Propagation. 369-383
- Ali Sinan Köksal, Viktor Kuncak, Philippe Suter: Scala to the Power of Z3: Integrating SMT and Programming. 400-406
- Lars Noschinski, Fabian Emmes, Jürgen Giesl: A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems. 422-438
- André Platzer: Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs. 446-460
- Michael Schneider, Geoff Sutcliffe: Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem Proving. 461-475
- Thomas Wies, Marco Muñiz, Viktor Kuncak: An Efficient Decision Procedure for Imperative Tree Data Structures. 476-491
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-18T214307 by the dblp team