| 2005 | A Combination Method for Generating Interpolants. Greta Yorsh, Madanlal Musuvathi |
| 2005 | A Focusing Inverse Method Theorem Prover for First-Order Linear Logic. Kaustuv Chaudhuri, Frank Pfenning |
| 2005 | A Proof-Producing Decision Procedure for Real Arithmetic. Sean McLaughlin, John Harrison |
| 2005 | An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard |
| 2005 | Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings Robert Nieuwenhuis |
| 2005 | Computer Search for Counterexamples to Wilkie's Identity. Jian Zhang |
| 2005 | Connecting Many-Sorted Theories. Franz Baader, Silvio Ghilardi |
| 2005 | Deciding Monodic Fragments by Temporal Resolution. Ullrich Hustadt, Boris Konev, Renate A. Schmidt |
| 2005 | Decision Procedures Customized for Formal Verification. Randal E. Bryant, Sanjit A. Seshia |
| 2005 | Deduction with XOR Constraints in Security API Modelling. Graham Steel |
| 2005 | Hierarchic Reasoning in Local Theory Extensions. Viorica Sofronie-Stokkermans |
| 2005 | KRHyper - In Your Pocket. Alex Sinner, Thomas Kleemann |
| 2005 | Model Representation via Contexts and Implicit Generalizations. Christian G. Fermüller, Reinhard Pichler |
| 2005 | Nominal Techniques in Isabelle/HOL. Christian Urban, Christine Tasson |
| 2005 | On the Complexity of Equational Horn Clauses. Kumar Neeraj Verma, Helmut Seidl, Thomas Schwentick |
| 2005 | Privacy-Sensitive Information Flow with JML. Guillaume Dufay, Amy P. Felty, Stan Matwin |
| 2005 | Proof Planning for First-Order Temporal Logic. Claudio Castellini, Alan Smaill |
| 2005 | Proving Properties of Incremental Merkle Trees. Mizuhito Ogawa, Eiichi Horita, Satoshi Ono |
| 2005 | Reasoning in Extensional Type Theory with Equality. Chad E. Brown |
| 2005 | Reflecting Proofs in First-Order Logic with Equality. Evelyne Contejean, Pierre Corbineau |
| 2005 | Regular Protocols and Attacks with Regular Knowledge. Tomasz Truderung |
| 2005 | Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures. Tal Lev-Ami, Neil Immerman, Thomas W. Reps, Shmuel Sagiv, Siddharth Srivastava, Greta Yorsh |
| 2005 | System Description: Multi A Multi-strategy Proof Planner. Andreas Meier, Erica Melis |
| 2005 | Tabling for Higher-Order Logic Programming. Brigitte Pientka |
| 2005 | Temporal Logics over Transitive States. Boris Konev, Frank Wolter, Michael Zakharyaschev |
| 2005 | Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules. Guillem Godoy, Ashish Tiwari |
| 2005 | The CoRe Calculus. Serge Autexier |
| 2005 | The Decidability of the First-Order Theory of Knuth-Bendix Order. Ting Zhang, Henny B. Sipma, Zohar Manna |
| 2005 | The MathSAT 3 System. Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani |
| 2005 | The Model Evolution Calculus with Equality. Peter Baumgartner, Cesare Tinelli |
| 2005 | The OWL Instance Store: System Description. Sean Bechhofer, Ian Horrocks, Daniele Turi |
| 2005 | Well-Nested Context Unification. Jordi Levy, Joachim Niehren, Mateu Villaret |
| 2005 | What Do We Know When We Know That a Theory Is Consistent?. Gilles Dowek |
| 2005 | sKizzo: A Suite to Evaluate and Certify QBFs. Marco Benedetti |