default search action
Christoph Walther
Person information
- affiliation: Darmstadt University of Technology, Germany
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2010 – 2019
- 2019
- [j8]Christoph Walther
:
Verified Newton-Raphson Iteration for Multiplicative Inverses Modulo Powers of Any Base. ACM Trans. Math. Softw. 45(1): 9:1-9:7 (2019) - 2018
- [c25]Christoph Walther
Formally Verified Montgomery Multiplication. CAV (2) 2018: 505-522 - 2017
- [j7]Christoph Walther
Fermat, Euler, Wilson - Three Case Studies in Number Theory. J. Autom. Reason. 59(2): 267-286 (2017)
2000 – 2009
- 2006
- [c24]Andreas Schlosser, Christoph Walther, Michael Gonder, Markus Aderhold:
Context Dependent Procedures and Computed Types in -eriFun. PLPV@IJCAR 2006: 61-78 - 2005
- [c23]Christoph Walther, Stephan Schweitzer:
Reasoning About Incompletely Defined Programs. LPAR 2005: 427-442 - 2004
- [j6]Christoph Walther, Stephan Schweitzer:
Verification in the Classroom. J. Autom. Reason. 32(1): 35-73 (2004) - [c22]Christoph Walther, Stephan Schweitzer:
Automated Termination Analysis for Incompletely Defined Programs. LPAR 2004: 332-346 - 2003
- [c21]Christoph Walther, Stephan Schweitzer:
About VeriFun. CADE 2003: 322-327 - [c20]Christoph Walther, Stephan Schweitzer:
A Machine-Verified Code Generator. LPAR 2003: 91-106 - [p2]Christoph Walther:
Automatisches Beweisen. Handbuch der Künstlichen Intelligenz 2003: 199-236 - 2001
- [b4]Christoph Walther:
Semantik und Programmverifikation. Teubner Texte zur Informatik 34, Teubner 2001, ISBN 3-519-00336-8 - 2000
- [j5]Christoph Walther, Thomas Kolbe:
Proving theorems by reuse. Artif. Intell. 116(1-2): 17-66 (2000) - [j4]Christoph Walther, Thomas Kolbe:
On Terminating Lemma Speculations. Inf. Comput. 162(1-2): 96-116 (2000) - [c19]Christoph Walther:
Criteria for Termination. Intellectics and Computational Logic 2000: 361-386
1990 – 1999
- 1996
- [c18]Thomas Kolbe, Christoph Walther:
Termination of Theorem Proving by Reuse. CADE 1996: 106-120 - 1995
- [c17]Thomas Kolbe, Christoph Walther:
Patching Proofs for Reuse (Extended Abstract). ECML 1995: 303-306 - [c16]Thomas Kolbe, Christoph Walther:
Second-Order Matching modulo Evaluation: A Technique for Reusing Proofs. IJCAI 1995: 190-195 - 1994
- [j3]Christoph Walther:
On Proving the Termination of Algorithms by Machine. Artif. Intell. 71(1): 101-157 (1994) - [c15]Thomas Kolbe, Christoph Walther:
Reusing Proofs. ECAI 1994: 80-84 - [p1]Christoph Walther:
Mathematical induction. Handbook of Logic in Artificial Intelligence and Logic Programming (2) 1994: 127-228 - 1993
- [c14]Christoph Walther:
Combining Induction Axioms by Machine. IJCAI 1993: 95-101 - 1992
- [c13]Christoph Walther:
Computing Induction Axioms. LPAR 1992: 381-392 - 1991
- [b3]Christoph Walther:
Automatisierung von Terminierungsbeweisen. Vieweg 1991, ISBN 3-528-04771-2
1980 – 1989
- 1989
- [c12]Christoph Walther:
Many-Sorted Inferences in Automated Theorem Proving. Sorts and Types in Artificial Intelligence 1989: 18-48 - 1988
- [j2]Christoph Walther:
Many-sorted unification. J. ACM 35(1): 1-17 (1988) - [c11]Christoph Walther:
Argument-Bounded Algorithms as a Basis for Automated Termination Proofs. CADE 1988: 602-621 - 1987
- [b2]Christoph Walther:
A Many-Sorted Calculus Based on Resolution and Paramodulation. Pitman / Morgan Kaufmann 1987, ISBN 0-273-08718-5 - [c10]Christoph Walther:
Many-Sorted Resolution. KIFS 1987: 65-102 - 1986
- [c9]Christoph Walther:
A Classification of Many-Sorted Unification Problems. CADE 1986: 525-537 - [c8]Susanne Biundo, Birgit Hummel, Dieter Hutter, Christoph Walther:
The Karlsruhe Induction Theorem Proving System. CADE 1986: 672-674 - [c7]Christoph Walther:
Automatisches Beweisen. KIFS 1986: 292-339 - 1985
- [j1]Christoph Walther:
A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution. Artif. Intell. 26(2): 217-224 (1985) - 1984
- [c6]Christoph Walther:
A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution. AAAI 1984: 330-334 - [c5]Christoph Walther:
Unification in Many-Sorted Theories. ECAI 1984: 383-392 - 1983
- [c4]Christoph Walther:
A Many-Sorted Calculus Based on Resolution and Paramodulation. IJCAI 1983: 882-891 - 1982
- [b1]Christoph Walther:
A many-sorted calculus based on resolution and paramodulation. Karlsruhe Institute of Technology, Germany, 1982 - 1981
- [c3]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 - [c2]Christoph Walther:
Elimination of Redundant Links in Extended Connection Graphs. GWAI 1981: 201-213 - 1980
- [c1]Norbert Eisinger, Jörg H. Siekmann, Gert Smolka, E. Unvericht, Christoph Walther:
Das Karlsruher Beweissystem. GI Jahrestagung 1980: 400-412
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-05-02 21:02 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: