| 2004 | Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure. | Guillem Godoy, Ashish Tiwari |
| 2004 | Efficient Algorithms for Constraint Description Problems over Finite Totally Ordered Domains: Extended Abstract. | ngel J. Gil, Miki Hermann, Gernot Salzer, Bruno Zanuttini |
| 2004 | Modular Proof Systems for Partial Functions with Weak Equality. | Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann |
| 2004 | Formalizing Undefinedness Arising in Calculus. | William M. Farmer |
| 2004 | Using Automated Theorem Provers to Certify Auto-generated Aerospace Software. | Ewen Denney, Bernd Fischer, Johann Schumann |
| 2004 | Automatic Generation of Classification Theorems for Finite Algebras. | Simon Colton, Andreas Meier, Volker Sorge, Roy L. McCasland |
| 2004 | TaMeD: A Tableau Method for Deduction Modulo. | Richard Bonichon |
| 2004 | Redundancy Notions for Paramodulation with Non-monotonic Orderings. | Miquel Bofill, Albert Rubio |
| 2004 | Adding Equivalence Classes to Stalmarck's Method in First Order Logic. | Magnus Bjrk |
| 2004 | Lambda Logic. | Michael Beeson |
| 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 | Formalizing O Notation in Isabelle/HOL. | Jeremy Avigad, Kevin Donnelly |
| 2004 | Efficient Algorithms for Computing Modulo Permutation Theories. | Jrgen Avenhaus |
| 2004 | Uniform variable splitting. | Roger Antonsen |
| 2003 | About VeriFun. | Christoph Walther, Stephan Schweitzer |
| 2003 | The CADE-19 ATP System Competition. | Geoff Sutcliffe, Christian B. Suttner |
| 2003 | Subset Types and Partial Functions. | Aaron Stump |
| 2003 | A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. | Renate A. Schmidt, Ullrich Hustadt |
| 2003 | Decidability of Arity-Bounded Higher-Order Matching. | Manfred Schmidt-Schau |
| 2003 | Matching in a Class of Combined Non-disjoint Theories. | Christophe Ringeissen |
| 2003 | Efficient Instance Retrieval with Standard and Relational Path Indexing. | Alexandre Riazanov, Andrei Voronkov |
| 2003 | Optimizing Higher-Order Pattern Unification. | Brigitte Pientka, Frank Pfenning |
| 2003 | Optimizing a BDD-Based Modal Solver. | Guoqiang Pan, Moshe Y. Vardi |
| 2003 | Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms. | Hans de Nivelle |