| 2005 | A First Order Extension of Stålmarck's Method. Magnus Björk |
| 2005 | A New Constraint Solver for 3D Lattices and Its Application to the Protein Folding Problem. Alessandro Dal Palù, Agostino Dovier, Enrico Pontelli |
| 2005 | A Unified Memory Model for Pointers. Harvey Tuch, Gerwin Klein |
| 2005 | Algebraic Intruder Deductions. David A. Basin, Sebastian Mödersheim, Luca Viganò |
| 2005 | An Algorithmic Account of Ehrenfeucht Games on Labeled Successor Structures. Angelo Montanari, Alberto Policriti, Nicola Vitacolonna |
| 2005 | Analytic Tableaux for KLM Preferential and Cumulative Logics. Laura Giordano, Valentina Gliozzi, Nicola Olivetti, Gian Luca Pozzato |
| 2005 | Another Complete Local Search Method for SAT. Haiou Shen, Hantao Zhang |
| 2005 | Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics. Wolfgang Ahrendt, Andreas Roth, Ralf Sasse |
| 2005 | Automating Coherent Logic. Marc Bezem, Thierry Coquand |
| 2005 | Bounding Resource Consumption with Gödel-Dummett Logics. Dominique Larchey-Wendling |
| 2005 | Characterizing Provability in . Didier Galmiche, Daniel Méry |
| 2005 | Comparative Similarity, Tree Automata, and Diophantine Equations. Mikhail Sheremet, Dmitry Tishkovsky, Frank Wolter, Michael Zakharyaschev |
| 2005 | Computational Issues in Exploiting Dependent And-Parallelism in Logic Programming: Leftness Detection in Dynamic Search Trees. Yao Wu, Enrico Pontelli, Desh Ranjan |
| 2005 | Concepts of Automata Construction from LTL. Carsten Fritz |
| 2005 | Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination. Chao Wang, Franjo Ivancic, Malay K. Ganai, Aarti Gupta |
| 2005 | Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. Robert Nieuwenhuis, Albert Oliveras |
| 2005 | Disjunctive Constraint Lambda Calculi. Matthias M. Hölzl, John N. Crossley |
| 2005 | Experimental Evaluation of Classical Automata Constructions. Deian Tabakov, Moshe Y. Vardi |
| 2005 | Functional Correctness Proofs of Encryption Algorithms. Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, Junxing Zhang |
| 2005 | Incremental Integrity Checking: Limitations and Possibilities. Henning Christiansen, Davide Martinenghi |
| 2005 | Independently Checkable Proofs from Decision Procedures: Issues and Progress. Allen Van Gelder |
| 2005 | Inference from Controversial Arguments. Sylvie Coste-Marquis, Caroline Devred, Pierre Marquis |
| 2005 | Integration of a Software Model Checker into Isabelle. Matthias Daum, Stefan Maus, Norbert Schirmer, Mohamed Nassim Seghir |
| 2005 | Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings Geoff Sutcliffe, Andrei Voronkov |
| 2005 | Matching with Regular Constraints. Temur Kutsia, Mircea Marin |
| 2005 | Model Checking Abstract State Machines with Answer Set Programming. Calvin Kai Fan Tang, Eugenia Ternovska |
| 2005 | Monotone AC-Tree Automata. Hitoshi Ohsaki, Jean-Marc Talbot, Sophie Tison, Yves Roos |
| 2005 | On Confluence of Infinitary Combinatory Reduction Systems. Jeroen Ketema, Jakob Grue Simonsen |
| 2005 | On Interpolation in Existence Logics. Matthias Baaz, Rosalie Iemhoff |
| 2005 | On the Finite Satisfiability Problem for the Guarded Fragment with Transitivity. Wieslaw Szwast, Lidia Tendera |
| 2005 | On the Specification of Sequent Systems. Elaine Pimentel, Dale Miller |
| 2005 | Optimizing the Runtime Processing of Types in Polymorphic Logic Programming Languages. Gopalan Nadathur, Xiaochu Qi |
| 2005 | Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning. Allen Van Gelder |
| 2005 | Programming Cognitive Agents in Defeasible Logic. Mehdi Dastani, Guido Governatori, Antonino Rotolo, Leendert W. N. van der Torre |
| 2005 | Pushdown Module Checking. Laura Bozzelli, Aniello Murano, Adriano Peron |
| 2005 | Reasoning About Incompletely Defined Programs. Christoph Walther, Stephan Schweitzer |
| 2005 | Recursive Path Orderings Can Also Be Incremental. Mirtha-Lina Fernández, Guillem Godoy, Albert Rubio |
| 2005 | Regular Derivations in Basic Superposition-Based Calculi. Vladimir Aleksic, Anatoli Degtyarev |
| 2005 | Satisfiability Checking for PC(ID). Maarten Mariën, Rudradeb Mitra, Marc Denecker, Maurice Bruynooghe |
| 2005 | Scaling Up: Computers vs. Common Sense. Douglas B. Lenat |
| 2005 | Second-Order Principles in Specification Languages for Object-Oriented Programs. Bernhard Beckert, Kerry Trentelman |
| 2005 | Strong Normalization of the Dual Classical Sequent Calculus. Daniel J. Dougherty, Silvia Ghilezan, Pierre Lescanne, Silvia Likavec |
| 2005 | Termination of Fair Computations in Term Rewriting. Salvador Lucas, José Meseguer |
| 2005 | The Four Sons of Penrose. Nachum Dershowitz |
| 2005 | The Relationship Between Reasoning About Privacy and Default Logics. Jürgen Dix, Wolfgang Faber, V. S. Subrahmanian |
| 2005 | The Theorema Environment for Interactive Proof Development. Florina Piroi, Temur Kutsia |
| 2005 | The nomore++ Approach to Answer Set Solving. Christian Anger, Martin Gebser, Thomas Linke, André Neumann, Torsten Schaub |
| 2005 | Towards Automated Proof Support for Probabilistic Distributed Systems. Annabelle McIver, Tjark Weber |
| 2005 | Treewidth in Verification: Local vs. Global. Andrea Ferrara, Guoqiang Pan, Moshe Y. Vardi |
| 2005 | Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic. Amine Chaieb, Tobias Nipkow |
| 2005 | Zap: Automated Theorem Proving for Software Analysis. Thomas Ball, Shuvendu K. Lahiri, Madanlal Musuvathi |