| 2005 | Privacy-Sensitive Information Flow with JML. | Guillaume Dufay, Amy P. Felty, Stan Matwin |
| 2005 | What Do We Know When We Know That a Theory Is Consistent?. | Gilles Dowek |
| 2005 | Reflecting Proofs in First-Order Logic with Equality. | Evelyne Contejean, Pierre Corbineau |
| 2005 | A Focusing Inverse Method Theorem Prover for First-Order Linear Logic. | Kaustuv Chaudhuri, Frank Pfenning |
| 2005 | Proof Planning for First-Order Temporal Logic. | Claudio Castellini, Alan Smaill |
| 2005 | Decision Procedures Customized for Formal Verification. | Randal E. Bryant, Sanjit A. Seshia |
| 2005 | Reasoning in Extensional Type Theory with Equality. | Chad E. Brown |
| 2005 | The MathSAT 3 System. | Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani |
| 2005 | sKizzo: A Suite to Evaluate and Certify QBFs. | Marco Benedetti |
| 2005 | The OWL Instance Store: System Description. | Sean Bechhofer, Ian Horrocks, Daniele Turi |
| 2005 | The Model Evolution Calculus with Equality. | Peter Baumgartner, Cesare Tinelli |
| 2005 | Connecting Many-Sorted Theories. | Franz Baader, Silvio Ghilardi |
| 2005 | The CoRe Calculus. | Serge Autexier |
| 2004 | Decision Procedures for Recursive Data Structures with Integer Constraints. | Ting Zhang, Henny B. Sipma, Zohar Manna |
| 2004 | Dr.Doodle: A Diagrammatic Theorem Prover. | Daniel Winterstein, Alan Bundy, Corin A. Gurr |
| 2004 | Dr.Doodle: A Diagrammatic Theorem Prover. | Daniel Winterstein |
| 2004 | Semantic Knowledge Partitioning. | Christoph Wernhard |
| 2004 | Solving Constraints by Elimination Methods. | Volker Weispfenning |
| 2004 | DPLL-based Procedure for Equality Logic with Uninterpreted Functions. | Olga Tveretin |
| 2004 | Sonic - Non-standard Inferences Go OilEd. | Anni-Yasmin Turhan, Christian Kissig |
| 2004 | Overlapping Leaf Permutative Equations. | Thierry Boy de la Tour, Mnacho Echenim |
| 2004 | Improved Modular Termination Proofs Using Dependency Pairs. | Ren Thiemann, Jrgen Giesl, Peter Schneider-Kamp |
| 2004 | Chain Resolution for the Semantic Web. | Tanel Tammet |
| 2004 | The CADE ATP System Competition. | Geoff Sutcliffe, Christian B. Suttner |
| 2004 | Analyzing Selected Quantified Integer Programs. | K. Subramani |