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 |