Christoph Walther

Christoph Walther
Born	August 9, 1950
Alma mater	Karlsruhe University
Thesis	A Many-Sorted Calculus Based on Resolution and Paramodulation (1984)
Doctoral advisor	Peter Deussen
Doctoral students	Jürgen Giesl, Josef Schneeberger
Known for	Walther recursion

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

Selected publications

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. 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. 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. 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) (VFR 02/01). TU Darmstadt.

• Christoph Walther and Stephan Schweitzer (2002). The VeriFun Tutorial (PDF) (Technical Report) (VFR 02/04). TU Darmstadt / Programmiermethodik.

• Christoph Walther and Stephan Schweitzer (2003). "About VeriFun" (PDF). In Franz Baader. 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. Proc. 8th CADE. LNAI 230. Springer. pp. 672—674.

• Christoph Walther (1992). "Computing Induction Axioms" (PDF). In Andrei Voronkov. Proc. LPAR. LNAI 624. Springer. pp. 381—392.

• Christoph Walther (1993). "Combining Induction Axioms by Machine" (PDF). In Ruzena Bajcsy. 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. Handbook of Logic in Artificial Intelligence and Logic Programming 2. Oxford University Press. pp. 127—227.

References

1. Simon Siegler and Nathan Wasser, ed. (2010). "Preface". Verification, Induction, Termination Analysis —- Festschrift for Christoph Walther on the Occasion of His 60th Birthday. LNAI 6463. Springer. ISBN 978-3-642-17171-0.
2. Professuren und Gruppenleitungen (Section Emeriti und Professoren im Ruhestand) at Darmstadt University Web Site

External links

• Christoph Walther at the Mathematics Genealogy Project
• Christoph Walther's home page at Darmstadt University