| 2004 | Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures. | Graham Steel, Alan Bundy, Monika Maidl |
| 2004 | System Description: E 0.81. | Stephan Schulz |
| 2004 | Efficient Checking of Term Ordering Constraints. | Alexandre Riazanov, Andrei Voronkov |
| 2004 | Reasoning Support for OWL-E. | Jeff Z. Pan |
| 2004 | The ICS Decision Procedures for Embedded Deduction. | Leonardo Mendona de Moura, Sam Owre, Harald Rue, John M. Rushby, Natarajan Shankar |
| 2004 | Understanding Higher Order Unification via Explicit Substitutions and Patterns. | Flvio L. C. de Moura |
| 2004 | Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools. | Jos Meseguer, Grigore Rosu |
| 2004 | Experiments on Supporting Interactive Proof Using Resolution. | Jia Meng, Lawrence C. Paulson |
| 2004 | Intelligent Theorem Proving for Specific Domains. | Paulo J. Matos |
| 2004 | argo-lib: A Generic Platform for Decision Procedures. | Filip Maric, Predrag Janicic |
| 2004 | PDL with Negation of Atomic Programs. | Carsten Lutz, Dirk Walther |
| 2004 | A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting. | Bernd Lchner |
| 2004 | Model Checking Using Tabled Rewriting. | Zhiyao Liang |
| 2004 | An implementation of a tableau theorem prover for modal logics. | Zhen Li |
| 2004 | Reasoning with large numbers of individuals moves on: extending the instance store. | Lei Li |
| 2004 | Generalised Handling of Variables in Disconnection Tableaux. | Reinhold Letz, Gernot Stenz |
| 2004 | Counter-Model Search in Gdel-Dummett Logics. | Dominique Larchey-Wendling |
| 2004 | Proof Reuse for Program Verification Calculi. | Vladimir Klebanov |
| 2004 | A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards. | Yevgeny Kazakov, Hans de Nivelle |
| 2004 | A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards. | Yevgeny Kazakov |
| 2004 | TeMP: A Temporal Monodic Prover. | Ullrich Hustadt, Boris Konev, Alexandre Riazanov, Andrei Voronkov |
| 2004 | A Tableau System for the Description Logic SHIO. | Jan Hladik |
| 2004 | A Superposition View on Nelson-Oppen. | Thomas Hillenbrand |
| 2004 | Super Solutions in Constraint Programming. | Emmanuel Hebrard |
| 2004 | Second-Order Logic over Finite Structures - Report on a Research Programme. | Georg Gottlob |