![](https://dblp1.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp1.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp1.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp1.uni-trier.de/img/search.dark.16x16.png)
default search action
23rd CADE 2011: Wroclaw, Poland
- Nikolaj S. Bjørner, Viorica Sofronie-Stokkermans:
Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings. Lecture Notes in Computer Science 6803, Springer 2011, 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 - Peter Baumgartner, Cesare Tinelli
:
Model Evolution with Equality Modulo Built-in Theories. 85-100 - Armin Biere
, Florian Lonsing
, Martina Seidl:
Blocked Clause Elimination for QBF. 101-115 - 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 - Sascha Böhme, Michal Moskal:
Heaps and Data Structures: A Challenge for Automated Provers. 177-191 - 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 - Krystof Hoder, Andrei Voronkov:
Sine Qua Non for Large Theory Reasoning. 299-314 - 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 - Pavel Klinov, Bijan Parsia:
A Hybrid Method for Probabilistic Satisfiability. 354-368 - Konstantin Korovin, Andrei Voronkov:
Solving Systems of Linear Inequalities by Bound Propagation. 369-383 - Laura Kovács
, Georg Moser, Andrei Voronkov:
On Transfinite Knuth-Bendix Orders. 384-399 - Ali Sinan Köksal, Viktor Kuncak, Philippe Suter:
Scala to the Power of Z3: Integrating SMT and Programming. 400-406 - Zhiqiang Liu, Christopher Lynch
:
Efficient General Unification for XOR with Homomorphism. 407-421 - Lars Noschinski, Fabian Emmes, Jürgen Giesl
:
A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems. 422-438 - Étienne Payet, Fausto Spoto
:
Static Analysis of Android Programs. 439-445 - 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 - Sarah Winkler
, Aart Middeldorp
:
AC Completion with Termination Tools. 492-498 - Harald Zankl, Bertram Felgenhauer, Aart Middeldorp
:
CSI - A Confluence Tool. 499-505
![](https://dblp1.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.