Christoph Walther Explained
|
Birth Date: | 9 August 1950 |
Alma Mater: | Karlsruhe University |
Thesis Title: | A many-Sorted Calculus Based on Resolution and Paramodulation |
Thesis1 Url: | and |
Thesis2 Url: | )--> |
Thesis Year: | 1984 |
Doctoral Advisor: | Peter Deussen |
Known For: | Walther recursion |
Spouses: | )--> |
Partners: | )--> |
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]
Selected publications
- Book: Thomas Kolbe . Christoph Walther . Reusing Proofs . Anthony Cohn . Proc. of the 11th European Conf. on Artificial Intelligence (ECAI-11) . John Wiley and Sons . 80–84 . https://www.researchgate.net/publication/2269729_Reusing_Proofs . 1994 .
- Book: Thomas Kolbe . Christoph Walther . Adaption of Proofs for Reuse . Proc. AAAI 1995 Fall Symposium on Adaption of Knowledge for Reuse . The AAAI Press . 61–67 . https://aaai.org/papers/0010-fs95-04-010-adaptation-of-proofs-for-reuse/ . 1995 .
- Book: Thomas Kolbe . Christoph Walther . Proof Management and Retrieval . Proc. IJCAI- 14 Workshop on Formal Approaches to the Reuse of Plans, Proofs and Programs . Morgan Kaufmann . 1–5 . https://scholar.google.de/scholar_url?url=https://citeseerx.ist.psu.edu/document%3Frepid%3Drep1%26type%3Dpdf%26doi%3Ddb7b1eb9a12537123061cc04b1f3ef1a5ac48520&hl=de&sa=X&ei=FQnuZaTFHrrKsQLf1KKwAQ&scisig=AFWwaeZvb5ej4P8cgn9SULaJ4Y48&oi=scholarr . 1995 .
- Book: Thomas Kolbe . Christoph Walther . Second-Order Matching modulo Evaluation – A Technique for Reusing Proofs . Proc. 14th Intern. Joint Conf. on Artificial Intelligence (IJCAI-14) . Morgan Kaufmann . 190–195 . https://dl.acm.org/doi/10.5555/1625855.1625880 . 1995 .
- Book: Thomas Kolbe . Christoph Walther . Patching Proofs for Reuse . Proc. of the 8th European Conf. on Machine Learning (ECML-8) . Springer . LNAI . 912 . 303–306 . https://link.springer.com/chapter/10.1007/3-540-59286-5_73 . 1995 . 10.1007/3-540-59286-5_73 .
- Book: Thomas Kolbe . Christoph Walther . Termination of Theorem Proving by Reuse . M. A. McRobbie . J. K. Slaney . Proc. 13th Inter. Conf. on Automated Deduction (CADE-13) . Springer . LNAI . 1104 . 106–120 . https://link.springer.com/chapter/10.1007/3-540-61511-3_72 . 1996 . 10.1007/3-540-61511-3_72 . 978-3-540-61511-8 .
- Book: Thomas Kolbe . Christoph Walther . Proving Theorems by Mimicking a Human’s Skill . AAAI 1996 Spring Symposium on Acquisition, Learning and Demonstration . The AAAI Press . 50–56 . https://aaai.org/papers/0010-ss96-02-010-proving-theorems-by-mimicking-a-humans-skill/ . 1996 .
- Book: Thomas Kolbe . Christoph Walther . Proof Analysis, Generalization and Reuse . 189–219 . 9 . Automated Deduction - A Basis for Applications . 10.1007/978-94-017-0435-9_8 . . . Applied Logic Series . Dordrecht . Kluwer Academic Publishers . 1998. 978-90-481-5051-9 .
- Christoph Walther . Thomas Kolbe . On Terminating Lemma Speculations . Information and Computation . 162 . 1–2 . 96–116 . 2000 . 10.1006/inco.1999.2859 . free .
- Christoph Walther . Thomas Kolbe . Proving theorems by reuse . Artificial Intelligence . 116 . 1–2 . 17–66 . 2000 . 10.1016/S0004-3702(99)00096-X.
- Book: Christoph Walther . Automatisches Beweisen . 223–263 . Günther Görz . Einführung in die Künstliche Intelligenz . Addison-Wesley . 2003.
- Book: Christoph Walther . Argument-Bounded Algorithms as a Basis for Automated Termination Proofs . . Springer . . 310 . 602–621 . 1988 .
- Book: Christoph Walther . Automatisierung von Terminierungsbeweisen . 1–254 . . Künstliche Intelligenz . Vieweg . https://link.springer.com/book/10.1007/978-3-322-85404-9 . 1991 . 10.1007/978-3-322-85404-9 . 978-3-528-04771-9 .
- Christoph Walther . On Proving the Termination of Algorithms by Machine . . 70 . 1 . 1991 .
- Book: Jürgen Giesl . Christoph Walther . Jürgen Brauburger . Termination Analysis for Functional Programs . 135–164 . 10 . Automated Deduction - A Basis for Applications . 10.1007/978-94-017-0437-3_6 . . . Applied Logic Series . Dordrecht . Kluwer Academic Publishers . 1998. 978-90-481-5052-6 .
- Book: Christoph Walther . Criteria for Termination . 361–386 . S. Hölldobler . Intellectics and Computational Logic . Dordrecht . Kluwer Academic Publishers . 2000 .
- Book: Christoph Walther . Stephan Schweitzer . Automated Termination Analysis for Incompletely Defined Programs . . . Proc. 11th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) . Springer . LNAI . 3452 . 332–346 . http://verifun.de/documents . 2005 .
On the VeriFun verification system for functional programs
- Book: Christoph Walther and Stephan Schweitzer . About VeriFun . Franz Baader . . Springer . LNAI . 2741 . 322–327 . http://verifun.de/documents . 2003 .
- Christoph Walther . Stephan Schweitzer . Verification in the Classroom . Journal of Automated Reasoning . 31 . 1 . 35–73 . 2004 . 10.1016/0004-3702(85)90029-3 .
- Book: Christoph Walther . Stephan Schweitzer . A Machine-Verified Code Generator . . . Proc. 10th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-10) . Springer . LNAI . 2850 . 91–106 . http://verifun.de/documents . 2005 .
- Book: Christoph Walther . Stephan Schweitzer . Reasoning about Incompletely Defined Programs . . . Proc. 12th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-12) . Springer . LNAI . 3835 . 427–442 . http://verifun.de/documents . 2005 .
- Book: Markus Aderhold . Christoph Walther . Daniel Szallies . Andreas Schlosser . A Fast Disprover for VeriFun . Wolfgang Ahrendt . Peter Baumgartner . Hans de Nivelle . Proc. Workshop on Non-Theorems, Non-Validity, Non-Provability (DISPROVING-06) . 59–69 . http://verifun.de/documents . 2006 .
- Book: Andreas Schlosser . Christoph Walther . Markus Aderhold . Axiomatic Specifications in VeriFun . Serge Autexier . Heiko Mantel . Proc. 6th Verification Workshop (VERIFY-06) . 146–163 . https://www.researchgate.net/publication/252264225_Axiomatic_Specifications_in_VeriFun . 2006 .
- Andreas Schlosser . Christoph Walther . Michael Gonder . Markus Aderhold . Context Dependent Procedures and Computed Types in VeriFun . Electronic Notes in Theoretical Computer Science . 174 . 7 . 61–78 . 2007 . 10.1016/j.entcs.2006.10.038 .
- Christoph Walther . Nathan Wasser . Fermat, Euler, Wilson - Three Case Studies in Number Theory . Journal of Automated Reasoning . 59 . 2 . 267–286 . 2017 . 10.1007/s10817-016-9387-z .
- Book: Christoph Walther . Formally Verified Montgomery Multiplication . Hana Chockler . Georg Weissenbacher . Proc. of the 30th Intern. Conf. on Computer Aided Verification (CAV 2018) . Springer . LNAI . 10982 . 505–522 . 10.1007/978-3-319-96142-2_30 . http://verifun.de/documents . 2018 . 978-3-319-96141-5 .
- Christoph Walther . Verified Newton-Raphson Iteration for Multiplicative Inverses Modulo Powers of Any Base . ACM Transactions on Mathematical Software . 45 . 1 . 9:1–9:7 . 2019 . 10.1145/3301317 .
On many-sorted unification, resolution and paramodulation
- Book: Christoph Walther . A Many-Sorted Calculus based on Resolution and Paramodulation . Alan Bundy . Proc. of the 8th Intern. Joint Conf. on Artificial Intelligence (IJCAI-8) . Morgan Kaufmann . 882–891 . 1983 .
- Book: Christoph Walther . A Mechanical Solution of Schubert’s Steamroller by Many-Sorted Resolution . Proc. of the 4th National Conf. on Artificial Intelligence (AAAI-4) . Morgan Kaufmann . 330–334 . 1984 .
- Book: Christoph Walther . Unification in Many- Sorted Theories . Tim O’Shea . Proc. of the 6th European Conf. on Artificial Intelligence (ECAI-6) . North-Holland . 383–392 . 1984 .
- Walther, Christoph . A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution . Artif. Intell. . 26 . 2 . 217–224 . 1985 . 10.1016/0004-3702(85)90029-3 .
- Book: Christoph Walther . A Classification of Many-Sorted Unification Problems . Jörg Siekmann . Proc. of the 8th Inter. Conf. on Automated Deduction (CADE-8) . Springer . LNAI . 230 . 525–537 . 1986 .
- Book: Christoph Walther . A Many-Sorted Calculus Based on Resolution and Paramodulation . Pitman (London) and Morgan Kaufmann (Los Altos) . 1–170 . 1987 . 978-0-273-08718-2 .
- Christoph Walther . Many-Sorted Unification . J. ACM . 35 . 1 . 1–17 . 1988 . 10.1145/42267.45071 .
- Book: Christoph Walther . Many-Sorted Inferences in Automated Theorem Proving . K.-H. Bläsius . U. Hedtstück . C.-R. Rollinger . Sorts and Types in Artificial Intelligence . Springer . LNAI . 418 . 18–48 . 1990 .
- Christoph Walther . An Algorithm for Many-Sorted Unification (Errata to Many-Sorted Unification, J. ACM vol 35(1), 1988) . TU Darmstadt . Technical Report . 2016–11–28 . 2016 .
On induction proving
- Book: Susanne Biundo and Birgit Hummel and Dieter Hutter and Christoph Walther . The Karlsruhe Induction Theorem Proving System . J.H. Siekmann . Proc. 8th CADE . Springer . LNAI . 230 . 672–674 . 1986 .
- Book: Christoph Walther . Mathematical Induction . 668–672 . S. C. Shapiro . Encyclopedia of Artificial Intelligence . John Wiley and Sons . https://dl.acm.org/doi/book/10.5555/122836 . 1992 .
- Book: Christoph Walther . Computing Induction Axioms . Andrei Voronkov . Proc. LPAR . Springer . LNAI . 624 . 381–392 . http://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/publikationen/Computing_Induction_Axioms_LPAR-1992-web.pdf . 1992 .
- Book: Christoph Walther . Combining Induction Axioms by Machine . Ruzena Bajcsy . . Morgan Kaufmann . 95–101 . http://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/publikationen/Combining_Induction_Axioms_by_Machine_IJCAI-13_1993.pdf . 1993 .
- Book: Christoph Walther . Mathematical Induction . 127–227 . . Handbook of Logic in Artificial Intelligence and Logic Programming . Oxford University Press . 2 . http://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/publikationen/Handbook_LAI_LP-Mathematical_Induction.pdf . 1994 .
- Book: Christoph Walther . Semantik und Programmverifikation . 1–212 . Teubner Texte zur Informatik . TEUBNER-TEXTE zur Informatik . 34 . Teubner-Wiley . https://link.springer.com/book/10.1007/978-3-322-86768-1 . 2001 . 10.1007/978-3-322-86768-1 . 978-3-519-00336-6 .
External links
Notes and References
- Book: Simon Siegler and Nathan Wasser . Verification, Induction, Termination Analysis - - Festschrift for Christoph Walther on the Occasion of His 60th Birthday . Preface . Springer . . 6463 . 978-3-642-17171-0 . 2010 .
- https://www.informatik.tu-darmstadt.de/de/fachbereich/professuren-und-gruppenleitungen/#c6424 Professuren und Gruppenleitungen