Christoph Walther (born 9 August 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]

Christoph Walther
Born (1950-08-09) 9 August 1950 (age 74)
Alma materKarlsruhe University
Known forWalther recursion
Scientific career
Thesis A many-Sorted Calculus Based on Resolution and Paramodulation  (1984)
Doctoral advisorPeter Deussen

Selected publications

edit
  • Thomas Kolbe; Christoph Walther (1994). "Reusing Proofs". In Anthony Cohn (ed.). Proc. of the 11th European Conf. on Artificial Intelligence (ECAI-11). John Wiley and Sons. pp. 80–84.
  • Thomas Kolbe; Christoph Walther (1995). "Adaption of Proofs for Reuse". Proc. AAAI 1995 Fall Symposium on Adaption of Knowledge for Reuse. The AAAI Press. pp. 61–67.
  • Thomas Kolbe; Christoph Walther (1995). "Proof Management and Retrieval". Proc. IJCAI- 14 Workshop on Formal Approaches to the Reuse of Plans, Proofs and Programs. Morgan Kaufmann. pp. 1–5.
  • Thomas Kolbe; Christoph Walther (1995). "Second-Order Matching modulo Evaluation – A Technique for Reusing Proofs". Proc. 14th Intern. Joint Conf. on Artificial Intelligence (IJCAI-14). Morgan Kaufmann. pp. 190–195.
  • Thomas Kolbe; Christoph Walther (1995). "Patching Proofs for Reuse". Proc. of the 8th European Conf. on Machine Learning (ECML-8). LNAI. Vol. 912. Springer. pp. 303–306. doi:10.1007/3-540-59286-5_73.
  • Thomas Kolbe; Christoph Walther (1996). "Termination of Theorem Proving by Reuse". In M. A. McRobbie; J. K. Slaney (eds.). Proc. 13th Inter. Conf. on Automated Deduction (CADE-13). LNAI. Vol. 1104. Springer. pp. 106–120. doi:10.1007/3-540-61511-3_72. ISBN 978-3-540-61511-8.
  • Thomas Kolbe; Christoph Walther (1996). "Proving Theorems by Mimicking a Human's Skill". AAAI 1996 Spring Symposium on Acquisition, Learning and Demonstration. The AAAI Press. pp. 50–56.
  • Thomas Kolbe; Christoph Walther (1998). "Proof Analysis, Generalization and Reuse". In Wolfgang Bibel; Peter Schmitt (eds.). Automated Deduction - A Basis for Applications. Applied Logic Series. Vol. 9. Dordrecht: Kluwer Academic Publishers. pp. 189–219. doi:10.1007/978-94-017-0435-9_8. ISBN 978-90-481-5051-9.
  • Christoph Walther; Thomas Kolbe (2000). "On Terminating Lemma Speculations". Information and Computation. 162 (1–2): 96–116. doi:10.1006/inco.1999.2859.
  • Christoph Walther; Thomas Kolbe (2000). "Proving theorems by reuse". Artificial Intelligence. 116 (1–2): 17–66. doi:10.1016/S0004-3702(99)00096-X.
  • Christoph Walther (2003). "Automatisches Beweisen". In Günther Görz (ed.). Einführung in die Künstliche Intelligenz. Addison-Wesley. pp. 223–263.

On the VeriFun verification system for functional programs

edit

On many-sorted unification, resolution and paramodulation

edit
  • Christoph Walther (1983). "A Many-Sorted Calculus based on Resolution and Paramodulation". In Alan Bundy (ed.). Proc. of the 8th Intern. Joint Conf. on Artificial Intelligence (IJCAI-8). Morgan Kaufmann. pp. 882–891.
  • Christoph Walther (1984). "A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution". Proc. of the 4th National Conf. on Artificial Intelligence (AAAI-4). Morgan Kaufmann. pp. 330–334.
  • Christoph Walther (1984). "Unification in Many- Sorted Theories". In Tim O’Shea (ed.). Proc. of the 6th European Conf. on Artificial Intelligence (ECAI-6). North-Holland. pp. 383–392.
  • Walther, Christoph (1985). "A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution". Artif. Intell. 26 (2): 217–224. doi:10.1016/0004-3702(85)90029-3.
  • Christoph Walther (1986). "A Classification of Many-Sorted Unification Problems". In Jörg Siekmann (ed.). Proc. of the 8th Inter. Conf. on Automated Deduction (CADE-8). LNAI. Vol. 230. Springer. pp. 525–537.
  • Christoph Walther (1987). A Many-Sorted Calculus Based on Resolution and Paramodulation. Pitman (London) and Morgan Kaufmann (Los Altos). pp. 1–170. ISBN 978-0-273-08718-2.
  • Christoph Walther (1988). "Many-Sorted Unification". J. ACM. 35 (1): 1–17. doi:10.1145/42267.45071.
  • Christoph Walther (1990). "Many-Sorted Inferences in Automated Theorem Proving". In K.-H. Bläsius; U. Hedtstück; C.-R. Rollinger (eds.). Sorts and Types in Artificial Intelligence. LNAI. Vol. 418. Springer. pp. 18–48.
  • Christoph Walther (2016). An Algorithm for Many-Sorted Unification (Errata to Many-Sorted Unification, J. ACM vol 35(1), 1988) (Technical Report). TU Darmstadt.

On induction proving

edit

References

edit
  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. Vol. 6463. Springer. ISBN 978-3-642-17171-0.
  2. ^ Professuren und Gruppenleitungen Archived 2015-02-21 at the Wayback Machine (Section Emeriti und Professoren im Ruhestand) at Darmstadt University Web Site
edit