


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

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.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














