Christoph Walther: Difference between revisions

Christoph Walther
Christoph Walther
Born	9 August 1950 (age 74)
Alma mater	Karlsruhe University
Known for	Walther recursion
	Scientific career
Thesis	A many-Sorted Calculus Based on Resolution and Paramodulation (1984)
Doctoral advisor	Peter Deussen

Browse history interactively

← Previous edit Next edit →

Content deleted Content added

VisualWikitext

Inline

Revision as of 21:16, 10 March 2024

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

On automated theorem proving

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.
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.
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. Vol. 9. Dordrecht: Kluwer Academic Publishers. pp. 189–219. doi:10.1007/978-94-017-0435-9_8.
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 automated termination analysis

Christoph Walther (1988). "Argument-Bounded Algorithms as a Basis for Automated Termination Proofs". Proc. 9th Conference on Automated Deduction. LNAI. Vol. 310. Springer. pp. 602–621.
Christoph Walther (1991). "Automatisierung von Terminierungsbeweisen". In Wolfgang Bibel (ed.). Künstliche Intelligenz. Vieweg. pp. 1–254.
Christoph Walther (1991). "On Proving the Termination of Algorithms by Machine". Artificial Intelligence. 70 (1).
Jürgen Giesl; Christoph Walther; Jürgen Brauburger (1998). "Termination Analysis for Functional Programs". In Wolfgang Bibel; Peter Schmitt (eds.). Automated Deduction - A Basis for Applications. Vol. 10. Dordrecht: Kluwer Academic Publishers. pp. 135–164. doi:10.1007/978-94-017-0437-3_6.
Christoph Walther (2000). "Criteria for Termination". In S. Hölldobler (ed.). Intellectics and Computational Logic. Dordrecht: Kluwer Academic Publishers. pp. 361–386.
Christoph Walther; Stephan Schweitzer (2005). "Automated Termination Analysis for Incompletely Defined Programs". In Franz Baader; Andrei Voronkov (eds.). Proc. 11th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). LNAI. Vol. 3452. Springer. pp. 332–346.

On the VeriFun verification system for functional programs

Christoph Walther and Stephan Schweitzer (2003). "About VeriFun". In Franz Baader (ed.). Proc. 19th Conference on Automated Deduction. LNAI. Vol. 2741. Springer. pp. 322–327.
Christoph Walther; Stephan Schweitzer (2004). "Verification in the Classroom". Journal of Automated Reasoning. 31 (1): 35–73. doi:10.1016/0004-3702(85)90029-3.
Christoph Walther; Stephan Schweitzer (2005). "A Machine-Verified Code Generator". In Moshe Y. Vardi ; Andrei Voronkov (eds.). Proc. 10th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-10). LNAI. Vol. 2850. Springer. pp. 91–106.
Christoph Walther; Stephan Schweitzer (2005). "Reasoning about Incompletely Defined Programs". In Geoff Sutcliffe ; Andrei Voronkov (eds.). Proc. 12th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-12). LNAI. Vol. 3835. Springer. pp. 427–442.
Markus Aderhold; Christoph Walther; Daniel Szallies; Andreas Schlosser (2006). "A Fast Disprover for VeriFun". In Wolfgang Ahrendt; Peter Baumgartner; Hans de Nivelle (eds.). Proc. Workshop on Non-Theorems, Non-Validity, Non-Provability (DISPROVING-06). pp. 59–69.
Andreas Schlosser; Christoph Walther; Markus Aderhold (2006). "Axiomatic Specifications in VeriFun". In Serge Autexier; Heiko Mantel (eds.). Proc. 6th Verification Workshop (VERIFY-06). pp. 146–163.
Andreas Schlosser; Christoph Walther; Michael Gonder; Markus Aderhold (2007). "Context Dependent Procedures and Computed Types in VeriFun". Electronic Notes in Theoretical Computer Science. 174 (7): 61–78. doi:10.1016/j.entcs.2006.10.038.
Christoph Walther; Nathan Wasser (2017). "Fermat, Euler, Wilson - Three Case Studies in Number Theory". Journal of Automated Reasoning. 59 (2): 267–286. doi:10.1007/s10817-016-9387-z.
Christoph Walther (2018). "Formally Verified Montgomery Multiplication". In Hana Chockler; Georg Weissenbacher (eds.). Proc. of the 30th Intern. Conf. on Computer Aided Verification (CAV 2018). LNAI. Vol. 10982. Springer. pp. 505–522. doi:10.1007/978-3-319-96142-2_30.
Christoph Walther (2019). "Verified Newton-Raphson Iteration for Multiplicative Inverses Modulo Powers of Any Base". ACM Transactions on Mathematical Software (TOMS). 45 (1): 9:1–9:7. doi:10.1145/3301317.

On many-sorted unification, resolution and paramodulation

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.
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

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. Vol. 230. Springer. pp. 672–674.
Christoph Walther (1992). "Mathematical Induction". In S. C. Shapiro (ed.). Encyclopedia of Artificial Intelligence. John Wiley and Sons. pp. 668–672.
Christoph Walther (1992). "Computing Induction Axioms" (PDF). In Andrei Voronkov (ed.). Proc. LPAR. LNAI. Vol. 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 in Artificial Intelligence and Logic Programming. Vol. 2. Oxford University Press. pp. 127–227.
Christoph Walther (2001). "Semantik und Programmverifikation". Teubner Texte zur Informatik. Vol. 34. Teubner-Wiley. pp. 1–212.

References

^ 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.
^ Professuren und Gruppenleitungen Archived 2015-02-21 at the Wayback Machine (Section Emeriti und Professoren im Ruhestand) at Darmstadt University Web Site

External links

Christoph Walther's home page at Darmstadt University
VeriFun System at Darmstadt University

[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

[1]

[2]

@@ Line 52: / Line 52: @@
 ==Selected publications==
-===On automated program [[termination analysis]]===
+===On [[automated theorem proving]]===
+* {{cite book | author1=Thomas Kolbe | author2=Christoph Walther | contribution=Reusing Proofs | editor=Anthony Cohn | title=Proc. of the 11th European Conf. on Artificial Intelligence (ECAI-11) | publisher=John Wiley and Sons | pages=80-84 | contribution-url=https://www.researchgate.net/publication/2269729_Reusing_Proofs | year=1994 }}
+* {{cite book | author1=Thomas Kolbe | author2=Christoph Walther | contribution=Adaption of Proofs for Reuse | title=Proc. AAAI 1995 Fall Symposium on Adaption of Knowledge for Reuse | publisher=The AAAI Press | pages=61-67 | contribution-url=https://aaai.org/papers/0010-fs95-04-010-adaptation-of-proofs-for-reuse/ | year=1995 }}
+* {{cite book | author1=Thomas Kolbe | author2=Christoph Walther | contribution=Proof Management and Retrieval | title=Proc. IJCAI- 14 Workshop on Formal Approaches to the Reuse of Plans, Proofs and Programs | publisher=Morgan Kaufmann | pages=1-5 | contribution-url=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 | year=1995 }}
+* {{cite book | author1=Thomas Kolbe | author2=Christoph Walther | contribution=Second-Order Matching modulo Evaluation – A Technique for Reusing Proofs | title=Proc. 14th Intern. Joint Conf. on Artificial Intelligence (IJCAI-14) | publisher=Morgan Kaufmann | pages=190-195 | contribution-url=https://dl.acm.org/doi/10.5555/1625855.1625880 | year=1995 }}
+* {{cite book | author1=Thomas Kolbe | author2=Christoph Walther | contribution=Patching Proofs for Reuse | title=Proc. of the 8th European Conf. on Machine Learning (ECML-8) | publisher=Springer | series=LNAI | volume=912 | pages=303–306 | contribution-url=https://link.springer.com/chapter/10.1007/3-540-59286-5_73 | year=1995 }}
+* {{cite book | author1=Thomas Kolbe | author2=Christoph Walther | contribution=Termination of Theorem Proving by Reuse | editor1=M. A. McRobbie |editor2=J. K. Slaney | title=Proc. 13th Inter. Conf. on Automated Deduction (CADE-13) | publisher=Springer | series=LNAI | volume=1104 | pages=106–120 | contribution-url=https://link.springer.com/chapter/10.1007/3-540-61511-3_72 | year=1996 }}
+* {{cite book | author1=Thomas Kolbe | author2=Christoph Walther | contribution=Proving Theorems by Mimicking a Human’s Skill | title=AAAI 1996 Spring Symposium on Acquisition, Learning and Demonstration | publisher=The AAAI Press | pages=50-56 | contribution-url=https://aaai.org/papers/0010-ss96-02-010-proving-theorems-by-mimicking-a-humans-skill/ | year=1996 }}
+* {{cite book | author1=Thomas Kolbe | author2=Christoph Walther | contribution=Proof Analysis, Generalization and Reuse | pages=189–219 | volume=9 |  url=https://link.springer.com/chapter/10.1007/978-94-017-0435-9_8 | doi=10.1007/978-94-017-0435-9_8 | editor1=[[Wolfgang Bibel]] |editor2=[[Peter Schmitt]] | title=Automated Deduction - A Basis for Applications | location=Dordrecht | publisher=Kluwer Academic Publishers | year=1998}}
+* {{cite journal | author1=Christoph Walther | author2=Thomas Kolbe | title=On Terminating Lemma Speculations | journal=Information and Computation | volume=162 | number=1-2 | pages=96–116 | year=2000 | doi=10.1006/inco.1999.2859 }}
+* {{cite journal | author1=Christoph Walther | author2=Thomas Kolbe | title=Proving theorems by reuse | journal=Artificial Intelligence | volume=116 | number=1-2 | pages=17–66 | year=2000 | doi=10.1016/S0004-3702(99)00096-X}}
+* {{cite book | author=Christoph Walther | contribution=Automatisches Beweisen | pages=223–263 | editor=Günther Görz | title=Einführung in die Künstliche Intelligenz | publisher=Addison-Wesley | year=2003}}
+===On automated [[termination analysis]]===
 * {{cite book | author=Christoph Walther | contribution=Argument-Bounded Algorithms as a Basis for Automated Termination Proofs | title=[[Conference on Automated Deduction|Proc. 9th Conference on Automated Deduction]] | publisher=Springer | series=[[LNAI]] | volume=310 | pages=602–621 | year=1988 }}
+* {{cite book | author=Christoph Walther | contribution=Automatisierung von Terminierungsbeweisen | pages=1–254 | editor=[[Wolfgang Bibel]] | title=Künstliche Intelligenz | publisher=Vieweg | contribution-url=https://link.springer.com/book/10.1007/978-3-322-85404-9 | year=1991 }}
 * {{cite journal | author=Christoph Walther | title=On Proving the Termination of Algorithms by Machine | journal=[[Artificial Intelligence (journal)|Artificial Intelligence]] | volume=70 | number=1 | year=1991 |url=http://verifun.de/documents }}
-* {{cite book | author=Jürgen Giesl |author2= Christoph Walther |author3= Jürgen Brauburger | contribution=Termination Analysis for Functional Programs | pages=135–164 | volume=3 |  url=https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=df17635172d349217c4a4dbc4d24a23c94ee85bc | editor=W. Bibel |editor2= P. Schmitt | title=Automated Deduction - A Basis for Applications | location=Dordrecht | publisher=Kluwer Academic Publishers | year=1998}}
+* {{cite book | author1=Jürgen Giesl |author2= Christoph Walther |author3= Jürgen Brauburger | contribution=Termination Analysis for Functional Programs | pages=135–164 | volume=10 |  url=https://link.springer.com/chapter/10.1007/978-94-017-0437-3_6 | doi=10.1007/978-94-017-0437-3_6 | editor1=[[Wolfgang Bibel]] |editor2=[[Peter Schmitt]] | title=Automated Deduction - A Basis for Applications | location=Dordrecht | publisher=Kluwer Academic Publishers | year=1998}}
 * {{cite book | author=Christoph Walther | contribution=Criteria for Termination | pages=361–386 |editor=S. Hölldobler | title=Intellectics and Computational Logic | location=Dordrecht | publisher=Kluwer Academic Publishers | year=2000 | url=http://verifun.de/documents}}
 * {{cite book | author1=Christoph Walther |author2= Stephan Schweitzer | contribution=Automated Termination Analysis for Incompletely Defined Programs | editor1=[[Franz Baader]] |editor2= [[Andrei Voronkov]] | title=Proc. 11th Int. Conf. on [[Logic for Programming, Artificial Intelligence and Reasoning]] (LPAR) | publisher=Springer | series=LNAI | volume=3452 | pages=332–346 | contribution-url=http://verifun.de/documents | year=2005 }}
@@ Line 62: / Line 77: @@
 ===On the ''VeriFun'' verification system for functional programs===
-* {{cite report | author=Christoph Walther and Stephan Schweitzer | title=VeriFun User Guide | institution=TU Darmstadt | type=Technical Report | number=VFR 02/01 | url=http://verifun.de/documents | year=2002 }}
-* {{cite report | author=Christoph Walther and Stephan Schweitzer | title=The VeriFun Tutorial | institution=TU Darmstadt / Programmiermethodik | type=Technical Report | number=VFR 02/04 | url=http://verifun.de/documents | year=2002 }}
 * {{cite book | author=Christoph Walther and Stephan Schweitzer | contribution=About VeriFun | editor=Franz Baader | title=Proc. 19th [[Conference on Automated Deduction]] | publisher=Springer | series=LNAI | volume=2741 | pages=322–327 | contribution-url=http://verifun.de/documents | year=2003 }}
 * {{cite journal | author1=Christoph Walther |author2= Stephan Schweitzer | title=Verification in the Classroom | journal=Journal of Automated Reasoning | volume=31 | number=1 | pages=35–73 | year=2004 | doi=10.1016/0004-3702(85)90029-3 | url=http://verifun.de/documents }}
@@ Line 69: / Line 82: @@
 * {{cite book | author1=Christoph Walther |author2= Stephan Schweitzer | contribution=Reasoning about Incompletely Defined Programs | editor1=[[Geoff Sutcliffe ]] |editor2= [[Andrei Voronkov]] | title=Proc. 12th Int. Conf. on [[Logic for Programming, Artificial Intelligence and Reasoning]] (LPAR-12) | publisher=Springer | series=LNAI | volume=3835 | pages=427–442 | contribution-url=http://verifun.de/documents | year=2005 }}
 * {{cite book | author1=Markus Aderhold |author2= Christoph Walther | author3=Daniel Szallies |author4= Andreas Schlosser | contribution=A Fast Disprover for VeriFun | editor1=Wolfgang Ahrendt |editor2= [[Peter Baumgartner]] | editor3= Hans de Nivelle | title=Proc. Workshop on Non-Theorems, Non-Validity, Non-Provability (DISPROVING-06) | pages=59–69 | contribution-url=http://verifun.de/documents | year=2006 }}
+* {{cite book | author1=Andreas Schlosser |author2= Christoph Walther | author3=Markus Aderhold | contribution=Axiomatic Specifications in VeriFun | editor1=Serge Autexier |editor2= Heiko Mantel | title=Proc. 6th Verification Workshop (VERIFY-06) | pages=146–163 | contribution-url=https://www.researchgate.net/publication/252264225_Axiomatic_Specifications_in_VeriFun | year=2006 }}
+* {{cite journal | author1=Andreas Schlosser |author2= Christoph Walther | author3=Michael Gonder |author4= Markus Aderhold | title=Context Dependent Procedures and Computed Types in VeriFun | journal=Electronic Notes in Theoretical Computer Science | volume=174 | number=7 | pages=61–78 | year=2007 | doi=10.1016/j.entcs.2006.10.038 | url=https://www.sciencedirect.com/science/article/pii/S1571066107002538 }}
 * {{cite journal | author1=Christoph Walther |author2= Nathan Wasser | title=Fermat, Euler, Wilson - Three Case Studies in Number Theory | journal=Journal of Automated Reasoning | volume=59 | number=2 | pages=267–286 | year=2017 | doi=10.1007/s10817-016-9387-z | url=http://verifun.de/documents }}
 * {{cite book | author=Christoph Walther | contribution=Formally Verified Montgomery Multiplication | editor1=Hana Chockler |editor2= Georg Weissenbacher | title=Proc. of the 30th Intern. Conf. on [[Computer Aided Verification]] (CAV 2018) | publisher=Springer | series=LNAI | volume=10982 | pages=505-522 | doi=10.1007/978-3-319-96142-2_30 | contribution-url=http://verifun.de/documents | year=2018 }}
 * {{cite journal | author=Christoph Walther | title=Verified Newton-Raphson Iteration for Multiplicative Inverses Modulo Powers of Any Base | journal=ACM Transactions on Mathematical Software (TOMS) | volume=45 | number=1 | pages=9:1–9:7 | year=2019 | doi=10.1145/3301317 | url=http://verifun.de/documents }}
+===On many-sorted unification, resolution and paramodulation===
-===On many-sorted resolution===
 * {{cite book | author=Christoph Walther | contribution=A Many-Sorted Calculus based on Resolution and Paramodulation | editor=Alan Bundy | title=Proc. of the 8th Intern. Joint Conf. on Artificial Intelligence (IJCAI-8) | publisher=Morgan Kaufmann | pages=882-891 | year=1983 }}
@@ Line 83: / Line 97: @@
 * {{cite book | author=Christoph Walther | title=A Many-Sorted Calculus Based on Resolution and Paramodulation | publisher=Pitman (London) and Morgan Kaufmann (Los Altos) | pages=1-170 | year=1987 | url=https://shop.elsevier.com/books/a-many-sorted-calculus-based-on-resolution-and-paramodulation/walther/978-0-273-08718-2 }}
 * {{cite journal | author=Christoph Walther | title=Many-Sorted Unification | journal=J.ACM | volume=35 | number=1 | pages=1–17 | year=1988 | doi=10.1145/42267.45071 }}
+* {{cite book | author=Christoph Walther | contribution=Many-Sorted Inferences in Automated Theorem Proving | editor1=K.-H. Bläsius | editor2=U. Hedtstück | editor3=C.-R. Rollinger | title=Sorts and Types in Artificial Intelligence | publisher=Springer | series=LNAI | volume=418 | pages=18-48 | year=1990 }}
+* {{cite report | author=Christoph Walther | title=An Algorithm for Many-Sorted Unification (Errata to Many-Sorted Unification, J.ACM vol 35(1), 1988) | institution=TU Darmstadt | type=Technical Report | number=2016-11-28 | url=https://www.researchgate.net/publication/331559488_An_Algorithm_for_Many-Sorted_Unification_Errata_to_Many-Sorted_Unification_JACM_vol_351_1988?channel=doi&linkId=5c804c78458515831f8b162d&showFulltext=true | year=2016 }}
 ===On induction proving===
 * {{cite book | author=[[Susanne Biundo-Stephan|Susanne Biundo]] and Birgit Hummel and Dieter Hutter and Christoph Walther | contribution=The Karlsruhe Induction Theorem Proving System | editor=J.H. Siekmann | title=Proc. 8th CADE | publisher=Springer | series=LNAI | volume=230 | pages=672–674 |  year=1986 }}
+* {{cite book | author=Christoph Walther | contribution=Mathematical Induction | pages=668–672 | editor=S. C. Shapiro | title=Encyclopedia of Artificial Intelligence | publisher=John Wiley and Sons | contribution-url=https://dl.acm.org/doi/book/10.5555/122836 | year=1992 }}
 * {{cite book | author=Christoph Walther | contribution=Computing Induction Axioms | editor=Andrei Voronkov | title=Proc. LPAR | publisher=Springer | series=LNAI | volume=624 | pages=381–392 | contribution-url=http://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/publikationen/Computing_Induction_Axioms_LPAR-1992-web.pdf | year=1992 }}
 * {{cite book | author=Christoph Walther | contribution=Combining Induction Axioms by Machine | editor=Ruzena Bajcsy | title=Proc. 13th [[IJCAI]] | publisher=Morgan Kaufmann | pages=95–101 | contribution-url=http://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/publikationen/Combining_Induction_Axioms_by_Machine_IJCAI-13_1993.pdf | year=1993 }}
 * {{cite book | author=Christoph Walther | contribution=Mathematical Induction | pages=127–227 | editor=[[Dov M. Gabbay]] and C.J. Hogger and [[J.A. Robinson]] | title=Handbook of Logic in Artificial Intelligence and Logic Programming | publisher=Oxford University Press | volume=2 | contribution-url=http://www.inferenzsysteme.informatik.tu-darmstadt.de/media/is/publikationen/Handbook_LAI_LP-Mathematical_Induction.pdf | year=1994 }}
+* {{cite book | author=Christoph Walther | contribution=Semantik und Programmverifikation | pages=1–212 | title=Teubner Texte zur Informatik | volume=34 | publisher=Teubner-Wiley | contribution-url=https://link.springer.com/book/10.1007/978-3-322-86768-1 | year=2001 }}
 ==References==
@@ Line 95: / Line 113: @@
 ==External links==
-* [http://www.inferenzsysteme.informatik.tu-darmstadt.de/mitarbeiter/christophwalther.de.jsp Christoph Walther's home page] at Darmstadt University
+* [https://www.informatik.tu-darmstadt.de/fb20/organisation_fb20/professuren_und_gruppenleitungen/fb20professuren_und_gruppenleitungen_detailseite_33664.de.jsp Christoph Walther's home page] at Darmstadt University
+* [http://www.verifun.de VeriFun System] at Darmstadt University
 {{Authority control}}

Authority control databases
International	ISNI VIAF FAST WorldCat
National	Germany United States Israel
Academics	Mathematics Genealogy Project DBLP MathSciNet
People	DDB
Other	IdRef