| 2007 |
| 34 | EE | Andreas Schlosser,
Christoph Walther,
Michael Gonder,
Markus Aderhold:
Context Dependent Procedures and Computed Types in -eriFun.
Electr. Notes Theor. Comput. Sci. 174(7): 61-78 (2007) |
| 2005 |
| 33 | EE | Christoph Walther,
Stephan Schweitzer:
Reasoning About Incompletely Defined Programs.
LPAR 2005: 427-442 |
| 2004 |
| 32 | EE | Christoph Walther,
Stephan Schweitzer:
Automated Termination Analysis for Incompletely Defined Programs.
LPAR 2004: 332-346 |
| 31 | EE | Christoph Walther,
Stephan Schweitzer:
Verification in the Classroom.
J. Autom. Reasoning 32(1): 35-73 (2004) |
| 2003 |
| 30 | EE | Christoph Walther,
Stephan Schweitzer:
About VeriFun.
CADE 2003: 322-327 |
| 29 | EE | Christoph Walther,
Stephan Schweitzer:
A Machine-Verified Code Generator.
LPAR 2003: 91-106 |
| 2001 |
| 28 | | Christoph Walther:
Semantik und Programmverifikation
Teubner 2001 |
| 2000 |
| 27 | | Christoph Walther:
Criteria for Termination.
Intellectics and Computational Logic 2000: 361-386 |
| 26 | EE | Christoph Walther,
Thomas Kolbe:
Proving theorems by reuse.
Artif. Intell. 116(1-2): 17-66 (2000) |
| 25 | | Christoph Walther,
Thomas Kolbe:
On Terminating Lemma Speculations.
Inf. Comput. 162(1-2): 96-116 (2000) |
| 1996 |
| 24 | | Thomas Kolbe,
Christoph Walther:
Termination of Theorem Proving by Reuse.
CADE 1996: 106-120 |
| 1995 |
| 23 | | Thomas Kolbe,
Christoph Walther:
Patching Proofs for Reuse (Extended Abstract).
ECML 1995: 303-306 |
| 22 | | Thomas Kolbe,
Christoph Walther:
Second-Order Matching modulo Evaluation: A Technique for Reusing Proofs.
IJCAI 1995: 190-195 |
| 1994 |
| 21 | | Thomas Kolbe,
Christoph Walther:
Reusing Proofs.
ECAI 1994: 80-84 |
| 20 | | Christoph Walther:
Mathematical induction.
Handbook of Logic in Artificial Intelligence and Logic Programming (2) 1994: 127-228 |
| 19 | | Christoph Walther:
On Proving the Termination of Algorithms by Machine.
Artif. Intell. 71(1): 101-157 (1994) |
| 1993 |
| 18 | | Christoph Walther:
Combining Induction Axioms by Machine.
IJCAI 1993: 95-101 |
| 1992 |
| 17 | | Christoph Walther:
Computing Induction Axioms.
LPAR 1992: 381-392 |
| 1991 |
| 16 | | Christoph Walther:
Automatisierung von Terminierungsbeweisen.
Vieweg 1991 |
| 1989 |
| 15 | | Christoph Walther:
Many-Sorted Inferences in Automated Theorem Proving.
Sorts and Types in Artificial Intelligence 1989: 18-48 |
| 1988 |
| 14 | | Christoph Walther:
Argument-Bounded Algorithms as a Basis for Automated Termination Proofs.
CADE 1988: 602-621 |
| 13 | EE | Christoph Walther:
Many-sorted unification.
J. ACM 35(1): 1-17 (1988) |
| 1987 |
| 12 | | Christoph Walther:
A Many-Sorted Calculus Based on Resolution and Paramodulation.
Pitman / Morgan Kaufmann 1987 |
| 11 | | Christoph Walther:
Many-Sorted Resolution.
KIFS 1987: 65-102 |
| 1986 |
| 10 | | Christoph Walther:
A Classification of Many-Sorted Unification Problems.
CADE 1986: 525-537 |
| 9 | | Susanne Biundo,
B. Hummel,
Dieter Hutter,
Christoph Walther:
The Karlsruhe Induction Theorem Proving System.
CADE 1986: 672-674 |
| 8 | | Christoph Walther:
Automatisches Beweisen.
KIFS 1986: 292-339 |
| 1985 |
| 7 | | Christoph Walther:
A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution.
Artif. Intell. 26(2): 217-224 (1985) |
| 1984 |
| 6 | | Christoph Walther:
A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution.
AAAI 1984: 330-334 |
| 5 | | Christoph Walther:
Unification in Many-Sorted Theories.
ECAI 1984: 383-392 |
| 1983 |
| 4 | | Christoph Walther:
A Many-Sorted Calculus Based on Resolution and Paramodulation.
IJCAI 1983: 882-891 |
| 1981 |
| 3 | | Christoph Walther:
Elimination of Redundant Links in Extended Connection Graphs.
GWAI 1981: 201-213 |
| 2 | | Karl-Hans Bläsius,
Norbert Eisinger,
Jörg H. Siekmann,
Gert Smolka,
Alexander Herold,
Christoph Walther:
The Markgraf Karl Refutation Procedure.
IJCAI 1981: 511-518 |
| 1980 |
| 1 | | Norbert Eisinger,
Jörg H. Siekmann,
Gert Smolka,
E. Unvericht,
Christoph Walther:
Das Karlsruher Beweissystem.
GI Jahrestagung 1980: 400-412 |