| 2004 | CADE | Generalised Handling of Variables in Disconnection Tableaux. | Reinhold Letz, Gernot Stenz |
| 2003 | TABLEAUX | Universal Variables in Disconnection Tableaux. | Reinhold Letz, Gernot Stenz |
| 2002 | TABLEAUX | Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas. | Reinhold Letz |
| 2002 | TABLEAUX | Integration of Equality Reasoning into the Disconnection Calculus. | Reinhold Letz, Gernot Stenz |
| 2001 | CADE | DCTP - A Disconnection Calculus Theorem Prover - System Abstract. | Reinhold Letz, Gernot Stenz |
| 2001 | LPAR | Automated Theorem Proving Proof and Model Generation with Disconnection Tableaux. | Reinhold Letz, Gernot Stenz |
| 1998 | CADE | Using Matings for Pruning Connection Tableaux. | Reinhold Letz |
| 1998 | FlAIRS | Strategy Parallelism in Automated Theorem Proving. | Andreas Wolf, Reinhold Letz |
| 1997 | TABLEAUX | Subgoal Alternation in Model Elimination. | Ortrun Ibens, Reinhold Letz |
| 1994 | CADE | SETHEO V3.2: Recent Developments - System Abstract. | Christoph Goller, Reinhold Letz, Klaus Mayr, Johann Schumann |
| 1993 | IJCAI | On the Polynomial Transparency of Resolution. | Reinhold Letz |
| 1992 | TABLEAUX | SETHEO II - The System and its Calculi. | Reinhold Letz, Klaus Mayr |
| 1990 | CADE | PARTHEO: A High-Performance Parallel Theorem Prover. | Johann Schumann, Reinhold Letz |
| 1990 | CADE | Tutorial on High-Performance Theorem Provers: Efficient Implementation and Parallelisation. | Johann Schumann, Reinhold Letz, Franz J. Kurfess |
| 1989 | WI | PARTHEO: A Parallel Inference Machine. | Stefan Bayerl, Reinhold Letz, Johann Schumann |
| 1986 | AIMSA | An Implementation of a PROLOG-like Theorem Prover based on the Connection Method. | Stefan Bayerl, Elmar Eder, Franz J. Kurfess, Reinhold Letz, Johann Schumann |