An Implementation of a PROLOG-like Theorem Prover based on the Connection Method. - Stefan Bayerl; Elmar Eder; Franz J. Kurfess; Reinhold Letz; Johann Schumann (AIMSA, 1986)

Expressing first order logic within Horn Clause logic - Reinhold Letz (Forschungsberichte, TU Munich, 1988)

PARTHEO: A Parallel Inference Machine. - Wolfgang Ertel; Franz J. Kurfess; Reinhold Letz; Xavier Pandolfi (PARLE (1), 1989)

PARTHEO: A Parallel Inference Machine. - Stefan Bayerl; Reinhold Letz; Johann Schumann (Wissensbasierte Systeme, 1989)

Classical negation in logic programming - Reinhold Letz (Forschungsberichte, TU Munich, 1989)

Tutorial on High-Performance Theorem Provers: Efficient Implementation and Parallelisation. - Johann Schumann; Reinhold Letz; Franz J. Kurfess (CADE, 1990)

Proof schemata in propositional calculi - Reinhold Letz; Klaus Mayr (Forschungsberichte, TU Munich, 1990)

PARTHEO: a high performance parallel theorem prover - Johann Schumann; Reinhold Letz (Forschungsberichte, TU Munich, 1990)

SETHEO II - The System and its Calculi. - Reinhold Letz; Klaus Mayr (TABLEAUX, 1992)

SETHEO: A High-Performance Theorem Prover. - Reinhold Letz; Johann Schumann; Stefan Bayerl; Wolfgang Bibel (J. Autom. Reason., 1992)

Connection tableaux and their relation with linear resolution - Reinhold Letz (Forschungsberichte, TU Munich, 1992)

On the polynomial transparency of resolution - Reinhold Letz (Forschungsberichte, TU Munich, 1992)

First-order calculi and proof procedures for automated deduction. - Reinhold Letz (1993)

SETHEO V3.2: Recent Developments - System Abstract. - Christoph Goller; Reinhold Letz; Klaus Mayr; Johann Schumann (CADE, 1994)

Cotrolled Integration of the Cut Rule into Connection Tableaux Calculi. - Reinhold Letz; Klaus Mayr; Christoph Goller (J. Autom. Reason., 1994)

Subgoal Alternation in Model Elimination. - Ortrun Ibens; Reinhold Letz (TABLEAUX, 1997)

LINUS - A Link Instantion Prover with Unit Support. - Reinhold Letz (J. Autom. Reason., 1997)

SETHEO and E-SETHEO - The CADE-13 Systems. - Max Moser; Ortrun Ibens; Reinhold Letz; Joachim Steinbach; Christoph Goller; Johann Schumann; Klaus Mayr (J. Autom. Reason., 1997)

Using Matings for Pruning Connection Tableaux. - Reinhold Letz (CADE, 1998)

Paradigmen und Perspektiven der automatischen Deduktion. - Reinhold Letz; Christoph Weidenbach (Künstliche Intell., 1998)

Strategy Parallelism in Automated Theorem Proving. - Andreas Wolf 005; Reinhold Letz (Int. J. Pattern Recognit. Artif. Intell., 1999)

Properties and Relations of Tableau and Connection Calculi. - Reinhold Letz (Intellectics and Computational Logic, 2000)

Model Elimination and Connection Tableau Procedures. - Reinhold Letz; Gernot Stenz (Handbook of Automated Reasoning, 2001)

DCTP - A Disconnection Calculus Theorem Prover - System Abstract. - Reinhold Letz; Gernot Stenz (IJCAR, 2001)

Automated Theorem Proving Proof and Model Generation with Disconnection Tableaux. - Reinhold Letz; Gernot Stenz (LPAR, 2001)

Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas. - Reinhold Letz (TABLEAUX, 2002)

Integration of Equality Reasoning into the Disconnection Calculus. - Reinhold Letz; Gernot Stenz (TABLEAUX, 2002)

Universal Variables in Disconnection Tableaux. - Reinhold Letz; Gernot Stenz (TABLEAUX, 2003)

Generalised Handling of Variables in Disconnection Tableaux. - Reinhold Letz; Gernot Stenz (IJCAR, 2004)

The Disconnection Tableau Calculus. - Reinhold Letz; Gernot Stenz (J. Autom. Reason., 2007)