Christoph Walther

Christoph Walther (born 9 August 1950) is a German computer scientist, known for his contributions to automated theorem proving. He is Professor emeritus at Darmstadt University of Technology.

On automated program termination analysis

• Christoph Walther (1988). "Argument-Bounded Algorithms as a Basis for Automated Termination Proofs". Proc. 9th Conference on Automated Deduction. LNAI. 310. Springer. pp. 602–621.
• Christoph Walther (1991). "On Proving the Termination of Algorithms by Machine" (PDF). Artificial Intelligence. 70 (1).
• Jürgen Giesl; Christoph Walther; Jürgen Brauburger (1998). "Termination Analysis for Functional Programs".In W. Bibel; P. Schmitt (eds.). Automated Deduction - A Basis for Applications (postscript). 3. Dordrecht: Kluwer Academic Publishers. pp. 135–164.
• Christoph Walther (2000). "Criteria for Termination".In S. Hölldobler (ed.). Intellectics and Computational Logic (postscript). Dordrecht: Kluwer Academic Publishers. pp. 361–386.
• Christoph Walther; Stephan Schweitzer (2005). "Automated Termination Analysis for Incompletely Defined Programs" (PDF).In Franz Baader; Andrei Voronkov (eds.). Proc. 11th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). LNAI. 3452. Springer. pp. 332–346.

On the VeriFun verification system for functional programs

• Christoph Walther and Stephan Schweitzer (2002). VeriFun User Guide (PDF) (Technical Report). TU Darmstadt.
• Christoph Walther and Stephan Schweitzer (2002). The VeriFun Tutorial (PDF) (Technical Report). TU Darmstadt / Programmiermethodik.
• Christoph Walther and Stephan Schweitzer (2003). "About VeriFun" (PDF).In Franz Baader (ed.). Proc. 19th Conference on Automated Deduction. LNAI. 2741. Springer. pp. 322–327.

On order-sorted resolution

• Walther, Christoph (1985). "A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution". Artif. Intell. 26 (2): 217–224.

On induction proving

• Susanne Biundo and Birgit Hummel and Dieter Hutter and Christoph Walther (1986). "The Karlsruhe Induction Theorem Proving System".In J.H. Siekmann (ed.). Proc. 8th CADE. LNAI. 230. Springer. pp. 672–674.
• Christoph Walther (1992). "Computing Induction Axioms" (PDF).In Andrei Voronkov (ed.). Proc. LPAR. LNAI. 624. Springer. pp. 381–392.
• Christoph Walther (1993). "Combining Induction Axioms by Machine" (PDF).In Ruzena Bajcsy (ed.). Proc. 13th IJCAI. Morgan Kaufmann. pp. 95–101.
• Christoph Walther (1994). "Mathematical Induction" (PDF).In Dov M. Gabbay and C.J. Hogger and J.A. Robinson (ed.). Handbook of Logic inArtificial Intelligence and Logic Programming. 2. Oxford University Press. pp. 127–227.