| 2009 | A Generalization of Semenov's Theorem to Automata over Real Numbers. Bernard Boigelot, Julien Brusten, Jérôme Leroux |
| 2009 | A Refined Resolution Calculus for CTL. Lan Zhang, Ullrich Hustadt, Clare Dixon |
| 2009 | A Tableau Calculus for Regular Grammar Logics with Converse. Linh Anh Nguyen, Andrzej Szalas |
| 2009 | A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs. Stephan Falke, Deepak Kapur |
| 2009 | An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability. Rajeev Goré, Florian Widmann |
| 2009 | Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings Renate A. Schmidt |
| 2009 | Automated Inference of Finite Unsatisfiability. Koen Claessen, Ann Lillieström |
| 2009 | Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis. Roberto Sebastiani, Michele Vescovi |
| 2009 | Beyond Dependency Graphs. Martin Korp, Aart Middeldorp |
| 2009 | Building Theorem Provers. Mark E. Stickel |
| 2009 | Combinable Extensions of Abelian Groups. Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch |
| 2009 | Complexity and Algorithms for Monomial and Clausal Predicate Abstraction. Shuvendu K. Lahiri, Shaz Qadeer |
| 2009 | Complexity of Fractran and Productivity. Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks |
| 2009 | Computing Knowledge in Security Protocols under Convergent Equational Theories. Stefan Ciobaca, Stéphanie Delaune, Steve Kremer |
| 2009 | Decidability Results for Saturation-Based Model Building. Matthias Horbach, Christoph Weidenbach |
| 2009 | Dei: A Theorem Prover for Terms with Integer Exponents. Hicham Bensaid, Ricardo Caferra, Nicolas Peltier |
| 2009 | Divvy: An ATP Meta-system Based on Axiom Relevance Ordering. Alex Roederer, Yury Puzis, Geoff Sutcliffe |
| 2009 | Does This Set of Clauses Overlap with at Least One MUS? Éric Grégoire, Bertrand Mazure, Cédric Piette |
| 2009 | Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method. Sean McLaughlin, Frank Pfenning |
| 2009 | Fair Derivations in Monodic Temporal Reasoning. Michel Ludwig, Ullrich Hustadt |
| 2009 | Ground Interpolation for Combined Theories. Amit Goel, Sava Krstic, Cesare Tinelli |
| 2009 | Instantiation-Based Automated Reasoning: From Theory to Practice. Konstantin Korovin |
| 2009 | Integrated Reasoning and Proof Choice Point Selection in the Jahob System - Mechanisms for Program Survival. Martin C. Rinard |
| 2009 | Interpolant Generation for UTVPI. Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani |
| 2009 | Interpolation and Symbol Elimination. Laura Kovács, Andrei Voronkov |
| 2009 | Locality Results for Certain Extensions of Theories with Bridging Functions. Viorica Sofronie-Stokkermans |
| 2009 | On Deciding Satisfiability by DPLL(G+ Maria Paola Bonacina, Christopher Lynch, Leonardo Mendonça de Moura |
| 2009 | Progress in the Development of Automated Theorem Proving for Higher-Order Logic. Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, Frank Theiss |
| 2009 | Real World Verification. André Platzer, Jan-David Quesel, Philipp Rümmer |
| 2009 | SPASS Version 3.5. Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, Patrick Wischnewski |
| 2009 | Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic. Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric Rodríguez-Carbonell, Albert Rubio |
| 2009 | Superposition and Model Evolution Combined. Peter Baumgartner, Uwe Waldmann |
| 2009 | System Description: H-PILoT. Carsten Ihlemann, Viorica Sofronie-Stokkermans |
| 2009 | Termination Analysis by Dependency Pairs and Inductive Theorem Proving. Stephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs, Peter Schneider-Kamp |
| 2009 | Volume Computation for Boolean Combination of Linear Arithmetic Constraints. Feifei Ma, Sheng Liu, Jian Zhang |
| 2009 | veriT: An Open, Trustable and Efficient SMT-Solver. Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine |