| 2007 | A Labelled System for IPL with Variable Splitting. Roger Antonsen, Arild Waaler |
| 2007 | An Incremental Technique for Automata-Based Decision Procedures. Gulay Ünel, David Toman |
| 2007 | Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings Frank Pfenning |
| 2007 | Automated Reasoning in Kleene Algebra. Peter Höfner, Georg Struth |
| 2007 | Automatic Decidability and Combinability Revisited. Christopher Lynch, Duc-Khanh Tran |
| 2007 | Automating Elementary Number-Theoretic Proofs Using Gröbner Bases. John Harrison |
| 2007 | Barendregt's Variable Convention in Rule Inductions. Christian Urban, Stefan Berghofer, Michael Norrish |
| 2007 | Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4. Samuli Heilala, Brigitte Pientka |
| 2007 | Certified Size-Change Termination. Alexander Krauss |
| 2007 | Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
| 2007 | Compilation as Rewriting in Higher Order Logic. Guodong Li, Konrad Slind |
| 2007 | Conservative Extensions in the Lightweight Description Logic EL. Carsten Lutz, Frank Wolter |
| 2007 | Dependency Pairs for Rewriting with Non-free Constructors. Stephan Falke, Deepak Kapur |
| 2007 | Designing Verification Conditions for Software. K. Rustan M. Leino |
| 2007 | Efficient E-Matching for SMT Solvers. Leonardo Mendonça de Moura, Nikolaj S. Bjørner |
| 2007 | Encoding First Order Proofs in SAT. Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin, Christopher Lynch, Ralph Eric McGregor |
| 2007 | Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. Juan Antonio Navarro Pérez, Andrei Voronkov |
| 2007 | Formalization of Continuous Probability Distributions. Osman Hasan, Sofiène Tahar |
| 2007 | Games, Automata and Matching. Colin Stirling |
| 2007 | Handling Polymorphism in Automated Deduction. Jean-François Couchot, Stéphane Lescuyer |
| 2007 | Hyper Tableaux with Equality. Peter Baumgartner, Ulrich Furbach, Björn Pelzer |
| 2007 | Improvements in Formula Generalization. Markus Aderhold |
| 2007 | KeY-C: A Tool for Verification of C Programs. Oleg Mürk, Daniel Larsson, Reiner Hähnle |
| 2007 | Labelled Clauses. Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv |
| 2007 | Logical Engineering with Instance-Based Methods. Peter Baumgartner |
| 2007 | Logical Interpretation: Static Program Analysis Using Theorem Proving. Ashish Tiwari, Sumit Gulwani |
| 2007 | On the Normalization and Unique Normalization Properties of Term Rewrite Systems. Guillem Godoy, Sophie Tison |
| 2007 | Optimized Reasoning in Description Logics Using Hypertableaux. Boris Motik, Robert D. C. Shearer, Ian Horrocks |
| 2007 | Predictive Labeling with Dependency Pairs Using SAT. Adam Koprowski, Aart Middeldorp |
| 2007 | Proving Termination by Bounded Increase. Jürgen Giesl, René Thiemann, Stephan Swiderski, Peter Schneider-Kamp |
| 2007 | SRASS - A Semantic Relevance Axiom Selection System. Geoff Sutcliffe, Yury Puzis |
| 2007 | Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. Yeting Ge, Clark W. Barrett, Cesare Tinelli |
| 2007 | System Description: E-KRHyper. Björn Pelzer, Christoph Wernhard |
| 2007 | System Description: SpassVersion 3.0. Christoph Weidenbach, Renate A. Schmidt, Thomas Hillenbrand, Rostislav Rusev, Dalibor Topic |
| 2007 | System for Automated Deduction (SAD): A Tool for Proof Verification. Konstantin Verchinine, Alexander V. Lyaletski, Andrey Paskevich |
| 2007 | T-Decision by Decomposition. Maria Paola Bonacina, Mnacho Echenim |
| 2007 | The Bedwyr System for Model Checking over Syntactic Expressions. David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu |
| 2007 | The KeY system 1.0 (Deduction Component). Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, Peter H. Schmitt |
| 2007 | Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. Viktor Kuncak, Martin C. Rinard |