| 2003 | 'Living Book': -'Deduction', 'Slicing', 'Interaction'. Peter Baumgartner, Ulrich Furbach, Margret Groß-Hardt, Alex Sinner |
| 2003 | A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. Renate A. Schmidt, Ullrich Hustadt |
| 2003 | A Randomized Satisfability Procedure for Arithmetic and Uninterpreted Function Symbols. Sumit Gulwani, George C. Necula |
| 2003 | A Translation of Looping Alternating Automata into Description Logics. Jan Hladik, Ulrike Sattler |
| 2003 | About VeriFun. Christoph Walther, Stephan Schweitzer |
| 2003 | Algorithms for Ordinal Arithmetic. Panagiotis Manolios, Daron Vroon |
| 2003 | An AC-Compatible Knuth-Bendix Order. Konstantin Korovin, Andrei Voronkov |
| 2003 | Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings Franz Baader |
| 2003 | Automating the Dependency Pair Method. Nao Hirokawa, Aart Middeldorp |
| 2003 | Canonization for Disjoint Unions of Theories. Sava Krstic, Sylvain Conchon |
| 2003 | Certifying Solutions to Permutation Group Problems. Arjeh M. Cohen, Scott H. Murray, Martin Pollet, Volker Sorge |
| 2003 | Decidability of Arity-Bounded Higher-Order Matching. Manfred Schmidt-Schauß |
| 2003 | Deciding Inductive Validity of Equations. Jürgen Giesl, Deepak Kapur |
| 2003 | Efficient Instance Retrieval with Standard and Relational Path Indexing. Alexandre Riazanov, Andrei Voronkov |
| 2003 | Equational Abstractions. José Meseguer, Miguel Palomino, Narciso Martí-Oliet |
| 2003 | Foundational Certified Code in a Metalogical Framework. Karl Crary, Susmit Sarkar |
| 2003 | How to Prove Inductive Theorems? QUODLIBET! Jürgen Avenhaus, Ulrich Kühler, Tobias Schmidt-Samoa, Claus-Peter Wirth |
| 2003 | IsaPlanner: A Prototype Proof Planner in Isabelle. Lucas Dixon, Jacques D. Fleuriot |
| 2003 | Matching in a Class of Combined Non-disjoint Theories. Christophe Ringeissen |
| 2003 | Monodic Temporal Resolution. Anatoli Degtyarev, Michael Fisher, Boris Konev |
| 2003 | Optimizing Higher-Order Pattern Unification. Brigitte Pientka, Frank Pfenning |
| 2003 | Optimizing a BDD-Based Modal Solver. Guoqiang Pan, Moshe Y. Vardi |
| 2003 | Proof Search and Proof Check for Equational and Inductive Theorems. Eric Deplagne, Claude Kirchner, Hélène Kirchner, Quang Huy Nguyen |
| 2003 | Proving Pointer Programs in Higher-Order Logic. Farhad Mehta, Tobias Nipkow |
| 2003 | Reasoning about Iteration in Gödel's Class Theory. Johan G. F. Belinfante |
| 2003 | Reasoning about Qualitative Representations of Space and Time. Anthony G. Cohn |
| 2003 | Reasoning about Quantifiers by Matching in the E-graph. Greg Nelson |
| 2003 | SAT-Based Counterexample Guided Abstraction Refinement in Model Checking. Edmund M. Clarke |
| 2003 | Schematic Saturation for Decision and Unification Problems. Christopher Lynch |
| 2003 | Source-Tracking Unification. Venkatesh Choppella, Christopher T. Haynes |
| 2003 | Subset Types and Partial Functions. Aaron Stump |
| 2003 | Superposition Modulo a Shostak Theory. Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann |
| 2003 | Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation. Harald Ganzinger, Jürgen Stuber |
| 2003 | TRP++2.0: A Temporal Resolution Prover. Ullrich Hustadt, Boris Konev |
| 2003 | The CADE-19 ATP System Competition. Geoff Sutcliffe, Christian B. Suttner |
| 2003 | The Complexity of Finite Model Reasoning in Description Logics. Carsten Lutz, Ulrike Sattler, Lidia Tendera |
| 2003 | The Homer System. Simon Colton, Sophie Huczynska |
| 2003 | The Model Evolution Calculus. Peter Baumgartner, Cesare Tinelli |
| 2003 | The New WALDMEISTER Loop at Work. Jean-Marie Gaillourdet, Thomas Hillenbrand, Bernd Löchner, Hendrik Spies |
| 2003 | Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms. Hans de Nivelle |
| 2003 | Unification Modulo ACU I Plus Homomorphisms/Distributivity. Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch |
| 2003 | adbmal Dimitri Hendriks, Vincent van Oostrom |