| 2006 | LPAR | Theory Instantiation. | Harald Ganzinger, Konstantin Korovin |
| 2004 | CADE | Modular Proof Systems for Partial Functions with Weak Equality. | Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann |
| 2004 | CAV | DPLL( T): Fast Decision Procedures. | Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli |
| 2004 | CSL | Integrating Equational Reasoning into Instantiation-Based Theorem Proving. | Harald Ganzinger, Konstantin Korovin |
| 2003 | CADE | Superposition Modulo a Shostak Theory. | Harald Ganzinger, Thomas Hillenbrand, Uwe Waldmann |
| 2003 | CADE | Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation. | Harald Ganzinger, Jrgen Stuber |
| 2003 | LICS | New Directions in Instantiation-Based Theorem Proving. | Harald Ganzinger, Konstantin Korovin |
| 2002 | CADE | Shostak Light. | Harald Ganzinger |
| 2002 | ICLP | Logical Algorithms. | Harald Ganzinger, David A. McAllester |
| 2001 | CADE | A New Meta-complexity Theorem for Bottom-Up Logic Programs. | Harald Ganzinger, David A. McAllester |
| 2001 | CADE | Context Trees. | Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela |
| 2001 | LICS | Relating Semantic and Proof-Theoretic Concepts for Polynominal Time Decidability of Uniform Word Problems. | Harald Ganzinger |
| 2001 | POPL | Efficient deductive methods for program analysis. | Harald Ganzinger |
| 1999 | ICALP | Decidable Fragments of Simultaneous Rigid Reachability. | Vronique Cortier, Harald Ganzinger, Florent Jacquemard, Margus Veanes |
| 1999 | LICS | The Two-Variable Guarded Fragment with Transitive Relations. | Harald Ganzinger, Christoph Meyer, Margus Veanes |
| 1999 | LICS | A Superposition Decision Procedure for the Guarded Fragment with Equality. | Harald Ganzinger, Hans de Nivelle |
| 1998 | AiML | A Resolution-Based Decision Procedure for Extensions of K4. | Harald Ganzinger, Ullrich Hustadt, Christoph Meyer, Renate A. Schmidt |
| 1998 | CADE | Strict Basic Superposition. | Leo Bachmair, Harald Ganzinger |
| 1998 | CADE | Elimination of Equality via Transformation with Ordering Constraints. | Leo Bachmair, Harald Ganzinger, Andrei Voronkov |
| 1997 | CADE | Soft Typing for Ordered Resolution. | Harald Ganzinger, Christoph Meyer, Christoph Weidenbach |
| 1996 | CADE | Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract). | Harald Ganzinger |
| 1996 | CADE | Theorem Proving in Cancellative Abelian Monoids (Extended Abstract). | Harald Ganzinger, Uwe Waldmann |
| 1996 | ICALP | Saturation-Based Theorem Proving (Abstract). | Harald Ganzinger |
| 1996 | LICS | Complexity Analysis Based on Ordered Resolution. | David A. Basin, Harald Ganzinger |
| 1994 | CADE | Ordered Chaining for Total Orderings. | Leo Bachmair, Harald Ganzinger |
| 1994 | COMPASS | Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings. | Leo Bachmair, Harald Ganzinger, Jrgen Stuber |
| 1994 | LICS | Rewrite Techniques for Transitive Relations | Leo Bachmair, Harald Ganzinger |
| 1993 | LICS | Set Constraints are the Monadic Class | Leo Bachmair, Harald Ganzinger, Uwe Waldmann |
| 1992 | CADE | Basic Paramodulation and Superposition. | Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder |
| 1992 | LPAR | Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria. | Leo Bachmair, Harald Ganzinger |
| 1991 | ICLP | Perfect Model Semantics for Logic Programs with Equality. | Leo Bachmair, Harald Ganzinger |
| 1990 | CADE | On Restrictions of Ordered Paramodulation with Simplification. | Leo Bachmair, Harald Ganzinger |
| 1990 | ICSE | System Support for Modular Order-Sorted Horn Clause Specifications. | Harald Ganzinger, Renate Schfers |
| 1988 | ESOP | CEC: A System for the Completion of Conditional Equational Specifications. | Hubert Bertling, Harald Ganzinger, Renate Schfers |
| 1987 | STACS | CEC (Conditional Equations Completion). | Hubert Bertling, Harald Ganzinger, Hubert Baumeister |
| 1987 | STACS | Ground Term Confluence in Parametric Conditional Equational Specifications. | Harald Ganzinger |
| 1986 | GI | Nichtprozedurale Sprachen und Probleme bei ihrer Implementierung (Kurzfassung). | Harald Ganzinger |
| 1986 | GI | Efficient Implementation of the Graphical Input/Output for Smalltalk-80. | Harald Ganzinger, Georg Heeg |
| 1983 | ICALP | Modular Compiler Descriptions Based on Abstract Semantic Data Types (Extended Abstract). | Harald Ganzinger |
| 1981 | GI | Description of Parameterized Compiler Modules. | Harald Ganzinger |
| 1981 | GI | Programs as Transformations of Algebraic Theories (Extended Abstract). | Harald Ganzinger |
| 1980 | CC | Transforming denotational semantics into practical attribute grammars. | Harald Ganzinger |
| 1979 | GI | An Approach to the Derivation of Compiler Descrition Concepts from the Mathematical Semantics Concept. | Harald Ganzinger |
| 1976 | ICSE | Design Evaluation of the Compiler Generating System MUGI. | Reinhard Wilhelm, Knut Ripken, Joachim Ciesinger, Harald Ganzinger, Walter Lahner, R. Nollmann |
| 1975 | GI | Verschrnkung von Compiler-Moduln. | Harald Ganzinger, Reinhard Wilhelm |