| 2005 | Scaling Up: Computers vs. Common Sense. | Douglas B. Lenat |
| 2005 | Bounding Resource Consumption with Gdel-Dummett Logics. | Dominique Larchey-Wendling |
| 2005 | Matching with Regular Constraints. | Temur Kutsia, Mircea Marin |
| 2005 | On Confluence of Infinitary Combinatory Reduction Systems. | Jeroen Ketema, Jakob Grue Simonsen |
| 2005 | Disjunctive Constraint Lambda Calculi. | Matthias M. Hlzl, John N. Crossley |
| 2005 | Analytic Tableaux for KLM Preferential and Cumulative Logics. | Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato |
| 2005 | Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning. | Allen Van Gelder |
| 2005 | Independently Checkable Proofs from Decision Procedures: Issues and Progress. | Allen Van Gelder |
| 2005 | Characterizing Provability in . | Didier Galmiche, Daniel Mry |
| 2005 | Concepts of Automata Construction from LTL. | Carsten Fritz |
| 2005 | Treewidth in Verification: Local vs. Global. | Andrea Ferrara, Guoqiang Pan, Moshe Y. Vardi |
| 2005 | Recursive Path Orderings Can Also Be Incremental. | Mirtha-Lina Fernndez, Guillem Godoy, Albert Rubio |
| 2005 | Functional Correctness Proofs of Encryption Algorithms. | Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, Junxing Zhang |
| 2005 | Strong Normalization of the Dual Classical Sequent Calculus. | Daniel J. Dougherty, Silvia Ghilezan, Pierre Lescanne, Silvia Likavec |
| 2005 | The Relationship Between Reasoning About Privacy and Default Logics. | Jrgen Dix, Wolfgang Faber, V. S. Subrahmanian |
| 2005 | The Four Sons of Penrose. | Nachum Dershowitz |
| 2005 | Integration of a Software Model Checker into Isabelle. | Matthias Daum, Stefan Maus, Norbert Schirmer, Mohamed Nassim Seghir |
| 2005 | Programming Cognitive Agents in Defeasible Logic. | Mehdi Dastani, Guido Governatori, Antonino Rotolo, Leendert W. N. van der Torre |
| 2005 | Inference from Controversial Arguments. | Sylvie Coste-Marquis, Caroline Devred, Pierre Marquis |
| 2005 | Incremental Integrity Checking: Limitations and Possibilities. | Henning Christiansen, Davide Martinenghi |
| 2005 | Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic. | Amine Chaieb, Tobias Nipkow |
| 2005 | Pushdown Module Checking. | Laura Bozzelli, Aniello Murano, Adriano Peron |
| 2005 | A First Order Extension of Stlmarck's Method. | Magnus Bjrk |
| 2005 | Automating Coherent Logic. | Marc Bezem, Thierry Coquand |
| 2005 | Second-Order Principles in Specification Languages for Object-Oriented Programs. | Bernhard Beckert, Kerry Trentelman |