165:
593:
568:
491:
1056:
1093:
1032:
1098:
912:
896:
931:
804:
1012:
975:
814:
704:
455:
399:
282:
232:
873:
and Birgit Hummel and Dieter Hutter and
Christoph Walther (1986). "The Karlsruhe Induction Theorem Proving System". In J.H. Siekmann (ed.).
845:
Christoph
Walther (1990). "Many-Sorted Inferences in Automated Theorem Proving". In K.-H. Bläsius; U. Hedtstück; C.-R. Rollinger (eds.).
1088:
117:
519:
415:
361:
1027:
1001:
Verification, Induction, Termination
Analysis —- Festschrift for Christoph Walther on the Occasion of His 60th Birthday
617:
243:
686:
130:
109:
746:
Christoph
Walther (1983). "A Many-Sorted Calculus based on Resolution and Paramodulation". In Alan Bundy (ed.).
428:
Jürgen Giesl; Christoph
Walther; Jürgen Brauburger (1998). "Termination Analysis for Functional Programs". In
152:
1083:
870:
794:
Christoph
Walther (1986). "A Classification of Many-Sorted Unification Problems". In Jörg Siekmann (ed.).
773:
Walther, Christoph (1985). "A Mechanical
Solution of Schubert's Steamroller by Many-Sorted Resolution".
755:
Christoph
Walther (1984). "A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution".
630:
1078:
359:
Christoph
Walther (1988). "Argument-Bounded Algorithms as a Basis for Automated Termination Proofs".
351:
50:
856:
An
Algorithm for Many-Sorted Unification (Errata to Many-Sorted Unification, J. ACM vol 35(1), 1988)
139:
113:
437:
264:
442:. Applied Logic Series. Vol. 10. Dordrecht: Kluwer Academic Publishers. pp. 135–164.
1008:
971:
810:
700:
451:
395:
278:
269:. Applied Logic Series. Vol. 9. Dordrecht: Kluwer Academic Publishers. pp. 189–219.
228:
60:
212:
191:
963:
833:
782:
727:
692:
667:
642:
541:
443:
387:
328:
305:
270:
220:
199:
90:
955:
375:
1036:
587:
583:
562:
485:
716:"Verified Newton-Raphson Iteration for Multiplicative Inverses Modulo Powers of Any Base"
170:
Proc. IJCAI- 14 Workshop on Formal Approaches to the Reuse of Plans, Proofs and Programs
764:
Christoph Walther (1984). "Unification in Many- Sorted Theories". In Tim O’Shea (ed.).
558:
429:
379:
256:
255:
Thomas Kolbe; Christoph Walther (1998). "Proof Analysis, Generalization and Reuse". In
332:
1072:
942:
938:
855:
786:
545:
433:
260:
108:(born 9 August 1950) is a German computer scientist, known for his contributions to
481:
696:
178:
646:
447:
274:
603:
Markus Aderhold; Christoph Walther; Daniel Szallies; Andreas Schlosser (2006).
967:
671:
629:
Andreas Schlosser; Christoph Walther; Michael Gonder; Markus Aderhold (2007).
465:
Christoph Walther (2000). "Criteria for Termination". In S. Hölldobler (ed.).
391:
962:. TEUBNER-TEXTE zur Informatik. Vol. 34. Teubner-Wiley. pp. 1–212.
883:
609:
Proc. Workshop on Non-Theorems, Non-Validity, Non-Provability (DISPROVING-06)
224:
203:
340:
Christoph Walther (2003). "Automatisches Beweisen". In Günther Görz (ed.).
310:
293:
179:"Second-Order Matching modulo Evaluation – A Technique for Reusing Proofs"
748:
Proc. of the 8th Intern. Joint Conf. on Artificial Intelligence (IJCAI-8)
837:
319:
Christoph Walther; Thomas Kolbe (2000). "Proving theorems by reuse".
248:
AAAI 1996 Spring Symposium on Acquisition, Learning and Demonstration
144:
Proc. of the 11th European Conf. on Artificial Intelligence (ECAI-11)
74:
731:
183:
Proc. 14th Intern. Joint Conf. on Artificial Intelligence (IJCAI-14)
809:. Pitman (London) and Morgan Kaufmann (Los Altos). pp. 1–170.
766:
Proc. of the 6th European Conf. on Artificial Intelligence (ECAI-6)
757:
Proc. of the 4th National Conf. on Artificial Intelligence (AAAI-4)
947:
Handbook of Logic in Artificial Intelligence and Logic Programming
921:
607:. In Wolfgang Ahrendt; Peter Baumgartner; Hans de Nivelle (eds.).
478:"Automated Termination Analysis for Incompletely Defined Programs"
157:
Proc. AAAI 1995 Fall Symposium on Adaption of Knowledge for Reuse
1004:
366:
715:
680:
655:
616:
Andreas Schlosser; Christoph Walther; Markus Aderhold (2006).
604:
579:
554:
529:
513:
477:
466:
410:
80:
A many-Sorted Calculus Based on Resolution and Paramodulation
806:
A Many-Sorted Calculus Based on Resolution and Paramodulation
796:
Proc. of the 8th Inter. Conf. on Automated Deduction (CADE-8)
656:"Fermat, Euler, Wilson - Three Case Studies in Number Theory"
631:"Context Dependent Procedures and Computed Types in VeriFun"
594:
Logic for Programming, Artificial Intelligence and Reasoning
569:
Logic for Programming, Artificial Intelligence and Reasoning
492:
Logic for Programming, Artificial Intelligence and Reasoning
196:
Proc. of the 8th European Conf. on Machine Learning (ECML-8)
471:. Dordrecht: Kluwer Academic Publishers. pp. 361–386.
949:. Vol. 2. Oxford University Press. pp. 127–227.
740:
On many-sorted unification, resolution and paramodulation
1062:
999:
Simon Siegler and Nathan Wasser, ed. (2010). "Preface".
217:
Proc. 13th Inter. Conf. on Automated Deduction (CADE-13)
824:
Christoph Walther (1988). "Many-Sorted Unification".
691:. LNAI. Vol. 10982. Springer. pp. 505–522.
411:"On Proving the Termination of Algorithms by Machine"
219:. LNAI. Vol. 1104. Springer. pp. 106–120.
598:. LNAI. Vol. 3835. Springer. pp. 427–442.
523:. LNAI. Vol. 2741. Springer. pp. 322–327.
496:. LNAI. Vol. 3452. Springer. pp. 332–346.
198:. LNAI. Vol. 912. Springer. pp. 303–306.
89:
73:
56:
46:
28:
21:
906:. LNAI. Vol. 624. Springer. pp. 381–392.
877:. LNAI. Vol. 230. Springer. pp. 672–674.
798:. LNAI. Vol. 230. Springer. pp. 525–537.
573:. LNAI. Vol. 2850. Springer. pp. 91–106.
512:Christoph Walther and Stephan Schweitzer (2003).
849:. LNAI. Vol. 418. Springer. pp. 18–48.
683:. In Hana Chockler; Georg Weissenbacher (eds.).
635:Electronic Notes in Theoretical Computer Science
580:"Reasoning about Incompletely Defined Programs"
244:"Proving Theorems by Mimicking a Human's Skill"
578:Christoph Walther; Stephan Schweitzer (2005).
553:Christoph Walther; Stephan Schweitzer (2005).
528:Christoph Walther; Stephan Schweitzer (2004).
476:Christoph Walther; Stephan Schweitzer (2005).
439:Automated Deduction - A Basis for Applications
266:Automated Deduction - A Basis for Applications
681:"Formally Verified Montgomery Multiplication"
8:
369:. Vol. 310. Springer. pp. 602–621.
622:Proc. 6th Verification Workshop (VERIFY-06)
506:verification system for functional programs
376:"Automatisierung von Terminierungsbeweisen"
362:Proc. 9th Conference on Automated Deduction
847:Sorts and Types in Artificial Intelligence
620:. In Serge Autexier; Heiko Mantel (eds.).
215:. In M. A. McRobbie; J. K. Slaney (eds.).
18:
720:ACM Transactions on Mathematical Software
654:Christoph Walther; Nathan Wasser (2017).
309:
213:"Termination of Theorem Proving by Reuse"
1099:Karlsruhe Institute of Technology alumni
890:. John Wiley and Sons. pp. 668–672.
342:Einführung in die Künstliche Intelligenz
292:Christoph Walther; Thomas Kolbe (2000).
242:Thomas Kolbe; Christoph Walther (1996).
211:Thomas Kolbe; Christoph Walther (1996).
190:Thomas Kolbe; Christoph Walther (1995).
177:Thomas Kolbe; Christoph Walther (1995).
164:Thomas Kolbe; Christoph Walther (1995).
151:Thomas Kolbe; Christoph Walther (1995).
138:Thomas Kolbe; Christoph Walther (1994).
1094:Technische Universität Darmstadt alumni
991:
913:"Combining Induction Axioms by Machine"
888:Encyclopedia of Artificial Intelligence
146:. John Wiley and Sons. pp. 80–84.
618:"Axiomatic Specifications in VeriFun"
16:German computer scientist (born 1950)
7:
1041:Emeriti und Professoren im Ruhestand
759:. Morgan Kaufmann. pp. 330–334.
750:. Morgan Kaufmann. pp. 882–891.
468:Intellectics and Computational Logic
185:. Morgan Kaufmann. pp. 190–195.
956:"Semantik und Programmverifikation"
925:. Morgan Kaufmann. pp. 95–101.
685:Proc. of the 30th Intern. Conf. on
555:"A Machine-Verified Code Generator"
344:. Addison-Wesley. pp. 223–263.
294:"On Terminating Lemma Speculations"
1043:) at Darmstadt University Web Site
768:. North-Holland. pp. 383–392.
118:Darmstadt University of Technology
14:
858:(Technical Report). TU Darmstadt.
520:Conference on Automated Deduction
250:. The AAAI Press. pp. 50–56.
159:. The AAAI Press. pp. 61–67.
1029:Professuren und Gruppenleitungen
172:. Morgan Kaufmann. pp. 1–5.
166:"Proof Management and Retrieval"
530:"Verification in the Classroom"
660:Journal of Automated Reasoning
605:"A Fast Disprover for VeriFun"
534:Journal of Automated Reasoning
153:"Adaption of Proofs for Reuse"
1:
1057:Christoph Walther's home page
333:10.1016/S0004-3702(99)00096-X
1007:. Vol. 6463. Springer.
960:Teubner Texte zur Informatik
902:. In Andrei Voronkov (ed.).
897:"Computing Induction Axioms"
787:10.1016/0004-3702(85)90029-3
697:10.1007/978-3-319-96142-2_30
546:10.1016/0004-3702(85)90029-3
687:Computer Aided Verification
647:10.1016/j.entcs.2006.10.038
448:10.1007/978-94-017-0437-3_6
298:Information and Computation
275:10.1007/978-94-017-0435-9_8
192:"Patching Proofs for Reuse"
1115:
1089:German computer scientists
954:Christoph Walther (2001).
930:Christoph Walther (1994).
918:. In Ruzena Bajcsy (ed.).
911:Christoph Walther (1993).
895:Christoph Walther (1992).
886:. In S. C. Shapiro (ed.).
882:Christoph Walther (1992).
854:Christoph Walther (2016).
803:Christoph Walther (1987).
714:Christoph Walther (2019).
679:Christoph Walther (2018).
409:Christoph Walther (1991).
386:. Vieweg. pp. 1–254.
374:Christoph Walther (1991).
968:10.1007/978-3-322-86768-1
672:10.1007/s10817-016-9387-z
592:Proc. 12th Int. Conf. on
567:Proc. 10th Int. Conf. on
516:. In Franz Baader (ed.).
490:Proc. 11th Int. Conf. on
392:10.1007/978-3-322-85404-9
142:. In Anthony Cohn (ed.).
131:automated theorem proving
110:automated theorem proving
99:
66:
932:"Mathematical Induction"
884:"Mathematical Induction"
225:10.1007/3-540-61511-3_72
204:10.1007/3-540-59286-5_73
1065:at Darmstadt University
1059:at Darmstadt University
416:Artificial Intelligence
321:Artificial Intelligence
384:Künstliche Intelligenz
311:10.1006/inco.1999.2859
124:Selected publications
941:and C.J. Hogger and
864:On induction proving
352:termination analysis
51:Karlsruhe University
838:10.1145/42267.45071
624:. pp. 146–163.
1035:2015-02-21 at the
114:Professor emeritus
1014:978-3-642-17171-0
977:978-3-519-00336-6
816:978-0-273-08718-2
706:978-3-319-96141-5
611:. pp. 59–69.
457:978-90-481-5052-6
401:978-3-528-04771-9
284:978-90-481-5051-9
234:978-3-540-61511-8
106:Christoph Walther
103:
102:
68:Scientific career
61:Walther recursion
23:Christoph Walther
1106:
1044:
1025:
1019:
1018:
996:
981:
950:
936:
926:
917:
907:
901:
891:
878:
859:
850:
841:
820:
799:
790:
769:
760:
751:
735:
710:
675:
650:
625:
612:
599:
574:
549:
524:
497:
472:
461:
424:
405:
370:
345:
336:
315:
313:
288:
251:
238:
207:
186:
173:
160:
147:
140:"Reusing Proofs"
91:Doctoral advisor
85:
42:
38:
36:
19:
1114:
1113:
1109:
1108:
1107:
1105:
1104:
1103:
1069:
1068:
1053:
1048:
1047:
1037:Wayback Machine
1026:
1022:
1015:
998:
997:
993:
988:
978:
953:
934:
929:
915:
910:
899:
894:
881:
869:
866:
853:
844:
823:
817:
802:
793:
772:
763:
754:
745:
742:
732:10.1145/3301317
713:
707:
678:
653:
628:
615:
602:
588:Andrei Voronkov
584:Geoff Sutcliffe
577:
563:Andrei Voronkov
552:
527:
514:"About VeriFun"
511:
508:
486:Andrei Voronkov
475:
464:
458:
427:
408:
402:
373:
358:
355:
339:
318:
304:(1–2): 96–116.
291:
285:
254:
241:
235:
210:
189:
176:
163:
150:
137:
134:
126:
83:
47:Alma mater
40:
34:
32:
24:
17:
12:
11:
5:
1112:
1110:
1102:
1101:
1096:
1091:
1086:
1081:
1071:
1070:
1067:
1066:
1063:VeriFun System
1060:
1052:
1051:External links
1049:
1046:
1045:
1020:
1013:
990:
989:
987:
984:
983:
982:
976:
951:
927:
908:
892:
879:
875:Proc. 8th CADE
871:Susanne Biundo
865:
862:
861:
860:
851:
842:
821:
815:
800:
791:
781:(2): 217–224.
770:
761:
752:
741:
738:
737:
736:
726:(1): 9:1–9:7.
711:
705:
676:
666:(2): 267–286.
651:
626:
613:
600:
575:
559:Moshe Y. Vardi
550:
525:
507:
500:
499:
498:
473:
462:
456:
430:Wolfgang Bibel
425:
406:
400:
380:Wolfgang Bibel
371:
354:
348:
347:
346:
337:
327:(1–2): 17–66.
316:
289:
283:
257:Wolfgang Bibel
252:
239:
233:
208:
187:
174:
161:
148:
133:
127:
125:
122:
101:
100:
97:
96:
93:
87:
86:
77:
71:
70:
64:
63:
58:
57:Known for
54:
53:
48:
44:
43:
30:
26:
25:
22:
15:
13:
10:
9:
6:
4:
3:
2:
1111:
1100:
1097:
1095:
1092:
1090:
1087:
1085:
1084:Living people
1082:
1080:
1077:
1076:
1074:
1064:
1061:
1058:
1055:
1054:
1050:
1042:
1038:
1034:
1031:
1030:
1024:
1021:
1016:
1010:
1006:
1002:
995:
992:
985:
979:
973:
969:
965:
961:
957:
952:
948:
944:
943:J.A. Robinson
940:
939:Dov M. Gabbay
933:
928:
924:
923:
914:
909:
905:
898:
893:
889:
885:
880:
876:
872:
868:
867:
863:
857:
852:
848:
843:
839:
835:
831:
827:
822:
818:
812:
808:
807:
801:
797:
792:
788:
784:
780:
776:
775:Artif. Intell
771:
767:
762:
758:
753:
749:
744:
743:
739:
733:
729:
725:
721:
717:
712:
708:
702:
698:
694:
690:
688:
682:
677:
673:
669:
665:
661:
657:
652:
648:
644:
640:
636:
632:
627:
623:
619:
614:
610:
606:
601:
597:
595:
589:
585:
581:
576:
572:
570:
564:
560:
556:
551:
547:
543:
539:
535:
531:
526:
522:
521:
515:
510:
509:
505:
501:
495:
493:
487:
483:
479:
474:
470:
469:
463:
459:
453:
449:
445:
441:
440:
435:
434:Peter Schmitt
431:
426:
422:
418:
417:
412:
407:
403:
397:
393:
389:
385:
381:
377:
372:
368:
364:
363:
357:
356:
353:
350:On automated
349:
343:
338:
334:
330:
326:
322:
317:
312:
307:
303:
299:
295:
290:
286:
280:
276:
272:
268:
267:
262:
261:Peter Schmitt
258:
253:
249:
245:
240:
236:
230:
226:
222:
218:
214:
209:
205:
201:
197:
193:
188:
184:
180:
175:
171:
167:
162:
158:
154:
149:
145:
141:
136:
135:
132:
128:
123:
121:
119:
115:
111:
107:
98:
95:Peter Deussen
94:
92:
88:
81:
78:
76:
72:
69:
65:
62:
59:
55:
52:
49:
45:
41:(age 74)
39:9 August 1950
31:
27:
20:
1040:
1028:
1023:
1000:
994:
959:
946:
919:
903:
887:
874:
846:
829:
825:
805:
795:
778:
774:
765:
756:
747:
723:
719:
684:
663:
659:
641:(7): 61–78.
638:
634:
621:
608:
591:
566:
540:(1): 35–73.
537:
533:
517:
503:
489:
482:Franz Baader
467:
438:
420:
414:
383:
360:
341:
324:
320:
301:
297:
265:
247:
216:
195:
182:
169:
156:
143:
105:
104:
79:
67:
1079:1950 births
920:Proc. 13th
832:(1): 1–17.
518:Proc. 19th
1073:Categories
986:References
904:Proc. LPAR
689:(CAV 2018)
35:1950-08-09
1039:(Section
596:(LPAR-12)
571:(LPAR-10)
1033:Archived
590:(eds.).
565:(eds.).
488:(eds.).
436:(eds.).
263:(eds.).
112:. He is
945:(ed.).
504:VeriFun
502:On the
382:(ed.).
1011:
974:
826:J. ACM
813:
703:
494:(LPAR)
454:
398:
281:
231:
84:(1984)
82:
75:Thesis
937:. In
935:(PDF)
922:IJCAI
916:(PDF)
900:(PDF)
582:. In
557:. In
480:. In
378:. In
1009:ISBN
1005:LNAI
972:ISBN
811:ISBN
701:ISBN
452:ISBN
423:(1).
396:ISBN
367:LNAI
279:ISBN
229:ISBN
29:Born
964:doi
834:doi
783:doi
728:doi
693:doi
668:doi
643:doi
639:174
542:doi
444:doi
388:doi
329:doi
325:116
306:doi
302:162
271:doi
221:doi
200:doi
129:On
116:at
1075::
1003:.
970:.
958:.
830:35
828:.
779:26
777:.
724:45
722:.
718:.
699:.
664:59
662:.
658:.
637:.
633:.
586:;
561:;
538:31
536:.
532:.
484:;
450:.
432:;
421:70
419:.
413:.
394:.
365:.
323:.
300:.
296:.
277:.
259:;
246:.
227:.
194:.
181:.
168:.
155:.
120:.
37:)
1017:.
980:.
966::
840:.
836::
819:.
789:.
785::
734:.
730::
709:.
695::
674:.
670::
649:.
645::
548:.
544::
460:.
446::
404:.
390::
335:.
331::
314:.
308::
287:.
273::
237:.
223::
206:.
202::
33:(
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.