| 2002 | A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code. Robert R. Schneck, George C. Necula |
| 2002 | A New Clausal Class Decidable by Hyperresolution. Lilia Georgieva, Ullrich Hustadt, Renate A. Schmidt |
| 2002 | A Note on Symmetry Heuristics in SEM. Thierry Boy de la Tour |
| 2002 | A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions. Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani |
| 2002 | Algorithmic Aspects of Herbrand Models Represented by Ground Atoms with Ground Equations. Bernhard Gramlich, Reinhard Pichler |
| 2002 | An LCF-Style Interface between HOL and First-Order Logic. Joe Hurd |
| 2002 | AutoBayes/CC - Combining Program Synthesis with Automatic Code Certification - System Description. Michael W. Whalen, Johann Schumann, Bernd Fischer |
| 2002 | Automated Deduction - CADE-18, 18th International Conference on Automated Deduction, Copenhagen, Denmark, July 27-30, 2002, Proceedings Andrei Voronkov |
| 2002 | BDD-Based Decision Procedures for K. Guoqiang Pan, Ulrike Sattler, Moshe Y. Vardi |
| 2002 | Basic Syntactic Mutation. Christopher Lynch, Barbara Morawska |
| 2002 | Combining Multisets with Integers. Calogero G. Zarba |
| 2002 | Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic. Dominique Larchey-Wendling |
| 2002 | Connection-Based Proof Search in Propositional BI Logic. Didier Galmiche, Daniel Méry |
| 2002 | DDDLIB: A Library for Solving Quantified Difference Inequalities. Jesper B. Møller |
| 2002 | Deductive Search for Errors in Free Data Type Specifications Using Model Generation. Wolfgang Ahrendt |
| 2002 | Embedding Lax Logic into Intuitionistic Logic. Uwe Egly |
| 2002 | Faster Proof Checking in the Edinburgh Logical Framework. Aaron Stump, David L. Dill |
| 2002 | Focussing Proof-Net Construction as a Middleware Paradigm. Jean-Marc Andreoli |
| 2002 | Formal Verification of a Combination Decision Procedure. Jonathan Ford, Natarajan Shankar |
| 2002 | Formal Verification of a Java Compiler in Isabelle. Martin Strecker |
| 2002 | HyLoRes 1.0: Direct Resolution for Hybrid Logics. Carlos Areces, Juan Heguiabehere |
| 2002 | Lazy Theorem Proving for Bounded Model Checking over Infinite Domains. Leonardo Mendonça de Moura, Harald Rueß, Maria Sorea |
| 2002 | Learn Omega-matic: System Description. Mateja Jamnik, Manfred Kerber, Martin Pollet |
| 2002 | Proof Analysis by Resolution. Matthias Baaz |
| 2002 | Proof Development with OMEGA. Jörg H. Siekmann, Christoph Benzmüller, Vladimir Brezhnev, Lassaad Cheikhrouhou, Armin Fiedler, Andreas Franke, Helmut Horacek, Michael Kohlhase, Andreas Meier, Erica Melis, Markus Moschner, Immanuel Normann, Martin Pollet, Volker Sorge, Carsten Ullrich, Claus-Peter Wirth, Jürgen Zimmer |
| 2002 | Reasoning by Symmetry and Function Ordering in Finite Model Generation. Gilles Audemard, Belaid Benhamou |
| 2002 | Reasoning with Expressive Description Logics: Theory and Practice. Ian Horrocks |
| 2002 | Recursive Path Orderings Can Be Context-Sensitive. Cristina Borralleras, Salvador Lucas, Albert Rubio |
| 2002 | S PASS Version 2.0. Christoph Weidenbach, Uwe Brahm, Thomas Hillenbrand, Enno Keen, Christian Theobalt, Dalibor Topic |
| 2002 | Shostak Light. Harald Ganzinger |
| 2002 | Solving for Set Variables in Higher-Order Theorem Proving. Chad E. Brown |
| 2002 | System Description: GrAnDe 1.0. Stephan Schulz, Geoff Sutcliffe |
| 2002 | System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning. Jürgen Zimmer, Michael Kohlhase |
| 2002 | Temporal Logic for Proof-Carrying Code. Andrew Bernard, Peter Lee |
| 2002 | Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points. Eugene Goldberg |
| 2002 | The Complexity of the Graded µ-Calculus. Orna Kupferman, Ulrike Sattler, Moshe Y. Vardi |
| 2002 | The HR Program for Theorem Generation. Simon Colton |
| 2002 | The Next W ALDMEISTER Loop. Thomas Hillenbrand, Bernd Löchner |
| 2002 | The Quest for Efficient Boolean Satisfiability Solvers. Lintao Zhang, Sharad Malik |
| 2002 | The Reflection Theorem: A Study in Meta-theoretic Reasoning. Lawrence C. Paulson |
| 2002 | Well-Foundedness Is Sufficient for Completeness of Ordered Paramodulation. Miquel Bofill, Albert Rubio |