| 2003 | Reasoning about Quantifiers by Matching in the E-graph. | Greg Nelson |
| 2003 | Equational Abstractions. | Jos Meseguer, Miguel Palomino, Narciso Mart-Oliet |
| 2003 | Proving Pointer Programs in Higher-Order Logic. | Farhad Mehta, Tobias Nipkow |
| 2003 | Algorithms for Ordinal Arithmetic. | Panagiotis Manolios, Daron Vroon |
| 2003 | Schematic Saturation for Decision and Unification Problems. | Christopher Lynch |
| 2003 | The Complexity of Finite Model Reasoning in Description Logics. | Carsten Lutz, Ulrike Sattler, Lidia Tendera |
| 2003 | Canonization for Disjoint Unions of Theories. | Sava Krstic, Sylvain Conchon |
| 2003 | An AC-Compatible Knuth-Bendix Order. | Konstantin Korovin, Andrei Voronkov |
| 2003 | TRP++2.0: A Temporal Resolution Prover. | Ullrich Hustadt, Boris Konev |
| 2003 | A Translation of Looping Alternating Automata into Description Logics. | Jan Hladik, Ulrike Sattler |
| 2003 | Automating the Dependency Pair Method. | Nao Hirokawa, Aart Middeldorp |
| 2003 | adbmal | Dimitri Hendriks, Vincent van Oostrom |
| 2003 | A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function Symbols. | Sumit Gulwani, George C. Necula |
| 2003 | Deciding Inductive Validity of Equations. | Jrgen Giesl, Deepak Kapur |
| 2003 | Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation. | Harald Ganzinger, Jrgen Stuber |
| 2003 | Superposition Modulo a Shostak Theory. | Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann |
| 2003 | The New WALDMEISTER Loop at Work. | Jean-Marie Gaillourdet, Thomas Hillenbrand, Bernd Lchner, Hendrik Spies |
| 2003 | IsaPlanner: A Prototype Proof Planner in Isabelle. | Lucas Dixon, Jacques D. Fleuriot |
| 2003 | Proof Search and Proof Check for Equational and Inductive Theorems. | Eric Deplagne, Claude Kirchner, Hlne Kirchner, Quang Huy Nguyen |
| 2003 | Monodic Temporal Resolution. | Anatoli Degtyarev, Michael Fisher, Boris Konev |
| 2003 | Foundational Certified Code in a Metalogical Framework. | Karl Crary, Susmit Sarkar |
| 2003 | The Homer System. | Simon Colton, Sophie Huczynska |
| 2003 | Reasoning about Qualitative Representations of Space and Time. | Anthony G. Cohn |
| 2003 | Certifying Solutions to Permutation Group Problems. | Arjeh M. Cohen, Scott H. Murray, Martin Pollet, Volker Sorge |
| 2003 | SAT-Based Counterexample Guided Abstraction Refinement in Model Checking. | Edmund M. Clarke |