| 2004 | A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. Gilles Barthe, Jan Cederquist, Sabrina Tarento |
| 2004 | A New Combination Procedure for the Word Problem That Generalizes Fusion Decidability Results in Modal Logics. Franz Baader, Silvio Ghilardi, Cesare Tinelli |
| 2004 | A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting. Bernd Löchner |
| 2004 | A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards. Yevgeny Kazakov, Hans de Nivelle |
| 2004 | Analyzing Selected Quantified Integer Programs. K. Subramani |
| 2004 | Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures. Graham Steel, Alan Bundy, Monika Maidl |
| 2004 | Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings David A. Basin, Michaël Rusinowitch |
| 2004 | Automatic Generation of Classification Theorems for Finite Algebras. Simon Colton, Andreas Meier, Volker Sorge, Roy L. McCasland |
| 2004 | Chain Resolution for the Semantic Web. Tanel Tammet |
| 2004 | Counter-Model Search in Gödel-Dummett Logics. Dominique Larchey-Wendling |
| 2004 | Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure. Guillem Godoy, Ashish Tiwari |
| 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 | Efficient Algorithms for Computing Modulo Permutation Theories. Jürgen Avenhaus |
| 2004 | Efficient Algorithms for Constraint Description Problems over Finite Totally Ordered Domains: Extended Abstract. Àngel J. Gil, Miki Hermann, Gernot Salzer, Bruno Zanuttini |
| 2004 | Efficient Checking of Term Ordering Constraints. Alexandre Riazanov, Andrei Voronkov |
| 2004 | Experiments on Supporting Interactive Proof Using Resolution. Jia Meng, Lawrence C. Paulson |
| 2004 | Formalizing O Notation in Isabelle/HOL. Jeremy Avigad, Kevin Donnelly |
| 2004 | Formalizing Undefinedness Arising in Calculus. William M. Farmer |
| 2004 | Generalised Handling of Variables in Disconnection Tableaux. Reinhold Letz, Gernot Stenz |
| 2004 | Improved Modular Termination Proofs Using Dependency Pairs. René Thiemann, Jürgen Giesl, Peter Schneider-Kamp |
| 2004 | Lambda Logic. Michael Beeson |
| 2004 | Modular Proof Systems for Partial Functions with Weak Equality. Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann |
| 2004 | Overlapping Leaf Permutative Equations. Thierry Boy de la Tour, Mnacho Echenim |
| 2004 | PDL with Negation of Atomic Programs. Carsten Lutz, Dirk Walther |
| 2004 | Redundancy Notions for Paramodulation with Non-monotonic Orderings. Miquel Bofill, Albert Rubio |
| 2004 | Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools. José Meseguer, Grigore Rosu |
| 2004 | Second-Order Logic over Finite Structures - Report on a Research Programme. Georg Gottlob |
| 2004 | Solving Constraints by Elimination Methods. Volker Weispfenning |
| 2004 | Sonic - Non-standard Inferences Go OilEd. Anni-Yasmin Turhan, Christian Kissig |
| 2004 | System Description: E 0.81. Stephan Schulz |
| 2004 | TaMeD: A Tableau Method for Deduction Modulo. Richard Bonichon |
| 2004 | TeMP: A Temporal Monodic Prover. Ullrich Hustadt, Boris Konev, Alexandre Riazanov, Andrei Voronkov |
| 2004 | The CADE ATP System Competition. Geoff Sutcliffe, Christian B. Suttner |
| 2004 | The ICS Decision Procedures for Embedded Deduction. Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar |
| 2004 | Using Automated Theorem Provers to Certify Auto-generated Aerospace Software. Ewen Denney, Bernd Fischer, Johann Schumann |
| 2004 | argo-lib: A Generic Platform for Decision Procedures. Filip Maric, Predrag Janicic |