| 2007 | Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. | Viktor Kuncak, Martin C. Rinard |
| 2007 | Certified Size-Change Termination. | Alexander Krauss |
| 2007 | Predictive Labeling with Dependency Pairs Using SAT. | Adam Koprowski, Aart Middeldorp |
| 2007 | Automated Reasoning in Kleene Algebra. | Peter Hfner, Georg Struth |
| 2007 | Extensional Reasoning. | Tim Hinrichs, Michael R. Genesereth |
| 2007 | Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4. | Samuli Heilala, Brigitte Pientka |
| 2007 | Formalization of Continuous Probability Distributions. | Osman Hasan, Sofine Tahar |
| 2007 | Automating Elementary Number-Theoretic Proofs Using Grbner Bases. | John Harrison |
| 2007 | Invited talk: Cyc Design Challenges and Solutions. | Keith Goolsbey |
| 2007 | On the Normalization and Unique Normalization Properties of Term Rewrite Systems. | Guillem Godoy, Sophie Tison |
| 2007 | Proving Termination by Bounded Increase. | Jrgen Giesl, Ren Thiemann, Stephan Swiderski, Peter Schneider-Kamp |
| 2007 | Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. | Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
| 2007 | Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. | Yeting Ge, Clark W. Barrett, Cesare Tinelli |
| 2007 | ALICE: An Advanced Logic for Interactive Component Engineering. | Borislav Gajanovic, Bernhard Rumpe |
| 2007 | Combinations of Theories and the Bernays-Schnfinkel-Ramsey Class. | Pascal Fontaine |
| 2007 | A Mechanization of Phylogenetic Trees. | Mamoun Filali |
| 2007 | Dependency Pairs for Rewriting with Non-free Constructors. | Stephan Falke, Deepak Kapur |
| 2007 | Encoding First Order Proofs in SAT. | Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin, Christopher Lynch, Ralph Eric McGregor |
| 2007 | Handling Polymorphism in Automated Deduction. | Jean-Franois Couchot, Stphane Lescuyer |
| 2007 | T-Decision by Decomposition. | Maria Paola Bonacina, Mnacho Echenim |
| 2007 | The KeY system 1.0 (Deduction Component). | Bernhard Beckert, Martin Giese, Reiner Hhnle, Vladimir Klebanov, Philipp Rmmer, Steffen Schlager, Peter H. Schmitt |
| 2007 | Hyper Tableaux with Equality. | Peter Baumgartner, Ulrich Furbach, Bjrn Pelzer |
| 2007 | Logical Engineering with Instance-Based Methods. | Peter Baumgartner |
| 2007 | The Bedwyr System for Model Checking over Syntactic Expressions. | David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu |
| 2007 | A Labelled System for IPL with Variable Splitting. | Roger Antonsen, Arild Waaler |