default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID22nd CADE 2009: Montreal, Canada
- Renate A. Schmidt:
Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. Lecture Notes in Computer Science 5663, Springer 2009, ISBN 978-3-642-02958-5
Invited Talk
- Martin C. Rinard:
Integrated Reasoning and Proof Choice Point Selection in the Jahob System - Mechanisms for Program Survival. 1-16
Combinations and Extensions
- Peter Baumgartner, Uwe Waldmann:
Superposition and Model Evolution Combined. 17-34 - Maria Paola Bonacina
, Christopher Lynch, Leonardo Mendonça de Moura:
On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving. 35-50 - Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch:
Combinable Extensions of Abelian Groups. 51-66 - Viorica Sofronie-Stokkermans:
Locality Results for Certain Extensions of Theories with Bridging Functions. 67-83
Minimal Unsatisfiability and Automated Reasoning Support
- Roberto Sebastiani, Michele Vescovi:
Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis. 84-99 - Éric Grégoire, Bertrand Mazure, Cédric Piette:
Does This Set of Clauses Overlap with at Least One MUS? 100-115 - Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, Frank Theiss:
Progress in the Development of Automated Theorem Proving for Higher-Order Logic. 116-130
System Descriptions
- Carsten Ihlemann, Viorica Sofronie-Stokkermans:
System Description: H-PILoT. 131-139 - Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, Patrick Wischnewski:
SPASS Version 3.5. 140-145 - Hicham Bensaid, Ricardo Caferra, Nicolas Peltier:
Dei: A Theorem Prover for Terms with Integer Exponents. 146-150 - Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine:
veriT: An Open, Trustable and Efficient SMT-Solver. 151-156 - Alex Roederer, Yury Puzis, Geoff Sutcliffe:
Divvy: An ATP Meta-system Based on Axiom Relevance Ordering. 157-162
Invited Talk
- Konstantin Korovin:
Instantiation-Based Automated Reasoning: From Theory to Practice. 163-166
Interpolation and Predicate Abstraction
- Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani:
Interpolant Generation for UTVPI. 167-182 - Amit Goel, Sava Krstic, Cesare Tinelli:
Ground Interpolation for Combined Theories. 183-198 - Laura Kovács, Andrei Voronkov:
Interpolation and Symbol Elimination. 199-213 - Shuvendu K. Lahiri, Shaz Qadeer:
Complexity and Algorithms for Monomial and Clausal Predicate Abstraction. 214-229
Resolution-Based Systems for Non-classical Logics
- Sean McLaughlin, Frank Pfenning:
Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method. 230-244 - Lan Zhang, Ullrich Hustadt, Clare Dixon:
A Refined Resolution Calculus for CTL. 245-260 - Michel Ludwig, Ullrich Hustadt:
Fair Derivations in Monodic Temporal Reasoning. 261-276
Termination Analysis and Constraint Solving
- Stephan Falke, Deepak Kapur:
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs. 277-293 - Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric Rodríguez-Carbonell, Albert Rubio:
Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic. 294-305
Invited Talk
- Mark E. Stickel:
Building Theorem Provers. 306-321
Rewriting, Termination and Productivity
- Stephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs, Peter Schneider-Kamp:
Termination Analysis by Dependency Pairs and Inductive Theorem Proving. 322-338 - Martin Korp, Aart Middeldorp:
Beyond Dependency Graphs. 339-354 - Stefan Ciobaca, Stéphanie Delaune, Steve Kremer:
Computing Knowledge in Security Protocols under Convergent Equational Theories. 355-370 - Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks:
Complexity of Fractran and Productivity. 371-387
Models
- Koen Claessen, Ann Lillieström:
Automated Inference of Finite Unsatisfiability. 388-403 - Matthias Horbach, Christoph Weidenbach:
Decidability Results for Saturation-Based Model Building. 404-420
Modal Tableaux with Global Caching
- Linh Anh Nguyen, Andrzej Szalas:
A Tableau Calculus for Regular Grammar Logics with Converse. 421-436 - Rajeev Goré, Florian Widmann:
An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability. 437-452
Arithmetic
- Feifei Ma, Sheng Liu, Jian Zhang:
Volume Computation for Boolean Combination of Linear Arithmetic Constraints. 453-468 - Bernard Boigelot, Julien Brusten, Jérôme Leroux:
A Generalization of Semenov's Theorem to Automata over Real Numbers. 469-484 - André Platzer, Jan-David Quesel, Philipp Rümmer:
Real World Verification. 485-501
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.
last updated on 2026-03-27 21:10 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
