| 2006 | Solving Sparse Linear Constraints. | Shuvendu K. Lahiri, Madanlal Musuvathi |
| 2006 | Partial Recursive Functions in Higher-Order Logic. | Alexander Krauss |
| 2006 | Automating Proofs in Category Theory. | Dexter Kozen, Christoph Kreitz, Eva Richter |
| 2006 | Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems. | Adam Koprowski, Hans Zantema |
| 2006 | A Resolution-Based Decision Procedure for | Yevgeny Kazakov, Boris Motik |
| 2006 | A Powerful Technique to Eliminate Isomorphism in Finite Model Search. | Xiangxue Jia, Jian Zhang |
| 2006 | System Description: GCLCprover + GeoThms. | Predrag Janicic, Pedro Quaresma |
| 2006 | Tree Automata with Equality Constraints Modulo Equational Theories. | Florent Jacquemard, Michal Rusinowitch, Laurent Vigneron |
| 2006 | A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms. | Joe Hendrix, Jos Meseguer, Hitoshi Ohsaki |
| 2006 | Towards Self-verification of HOL Light. | John Harrison |
| 2006 | Inferring Network Invariants Automatically. | Olga Grinchtein, Martin Leucker, Nir Piterman |
| 2006 | A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. | Benjamin Grgoire, Laurent Thry |
| 2006 | Automatic Termination Proofs in the Dependency Pair Framework. | Jrgen Giesl, Peter Schneider-Kamp, Ren Thiemann |
| 2006 | Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation. | Allen Van Gelder, Geoff Sutcliffe |
| 2006 | Matrix Interpretations for Proving Termination of Term Rewriting. | Jrg Endrullis, Johannes Waldmann, Hans Zantema |
| 2006 | Strong Cut-Elimination Systems for Hudelmaier's Depth-Bounded Sequent Calculus for Implicational Logic. | Roy Dyckhoff, Delia Kesner, Stphane Lengrand |
| 2006 | Specifying and Reasoning About Dynamic Access-Control Policies. | Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi |
| 2006 | Presburger Modal Logic Is PSPACE-Complete. | Stphane Demri, Denis Lugiez |
| 2006 | Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation. | Adnan Darwiche |
| 2006 | Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics. | Robert L. Constable, Wojciech Moczydlowski |
| 2006 | A Logical Characterization of Forward and Backward Chaining in the Inverse Method. | Kaustuv Chaudhuri, Frank Pfenning, Greg Price |
| 2006 | Verifying Mixed Real-Integer Quantifier Elimination. | Amine Chaieb |
| 2006 | Mathematical Theory Exploration. | Bruno Buchberger |
| 2006 | Combining Type Theory and Untyped Set Theory. | Chad E. Brown |
| 2006 | Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures. | Maria Paola Bonacina, Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |