クリストフ・ヴァルター

クリストフ・ヴァルター（1950年8月9日生まれ）^[1] はドイツのコンピュータ科学者であり、定理の自動証明への貢献で知られています。彼はダルムシュタット工科大学の名誉教授です。^[2]

• Thomas Kolbe、Christoph Walther (1994)。「証明の再利用」。Anthony Cohn (編)。第 11 回ヨーロッパ人工知能会議 (ECAI-11) 議事録。John Wiley and Sons。pp. 80–84。
• Thomas Kolbe、Christoph Walther (1995)。「再利用のための証明の適応」。AAAI 1995 年秋季シンポジウム「再利用のための知識の適応」議事録。AAAI プレス。pp. 61–67。
• Thomas Kolbe、Christoph Walther (1995)。「証明の管理と検索」。計画、証明、プログラムの再利用に対する形式的アプローチに関する IJCAI- 14 ワークショップ議事録。Morgan Kaufmann。pp. 1–5。
• Thomas Kolbe、Christoph Walther (1995)。「評価を法とする 2 次マッチング - 証明の再利用テクニック」。Proc . 14th Intern. Joint Conf. on Artificial Intelligence (IJCAI-14)。Morgan Kaufmann。pp. 190–195。
• Thomas Kolbe、Christoph Walther (1995)。「再利用のための証明のパッチング」。第8 回ヨーロッパ機械学習会議 (ECML-8) 議事録。LNAI。第 912 巻。Springer。pp. 303–306。doi :10.1007/3-540-59286-5_73。
• Thomas Kolbe、Christoph Walther (1996)。「再利用による定理証明の終了」。MA McRobbie、JK Slaney (編)。Proc . 13th Inter . Conf. on Automated Deduction (CADE-13)。LNAI。Vol. 1104。Springer。pp. 106–120。doi :10.1007/ 3-540-61511-3_72。ISBN 978-3-540-61511-8。
• Thomas Kolbe、Christoph Walther (1996)。「人間のスキルを模倣して定理を証明する」。AAAI 1996 春季シンポジウム、習得、学習、デモンストレーション。AAAI プレス。pp. 50–56。
• Thomas Kolbe、Christoph Walther (1998)。「証明分析、一般化、再利用」。Wolfgang Bibel、Peter Schmitt (編)。自動演繹 - アプリケーションの基礎。応用論理シリーズ。第 9 巻。ドルドレヒト: Kluwer Academic Publishers。pp. 189–219。doi : 10.1007 / 978-94-017-0435-9_8。ISBN 978-90-481-5051-9。
• Christoph Walther、Thomas Kolbe (2000)。 「終了する補題推測について」。情報と計算。162 (1–2): 96–116。doi : 10.1006/inco.1999.2859。
• Christoph Walther、Thomas Kolbe (2000)。「再利用による定理の証明」。人工知能。116 (1–2): 17–66。doi : 10.1016/S0004-3702(99)00096-X。
• クリストフ・ヴァルサー (2003)。 「オートマティッシェス・ベヴァイゼン」。ギュンター・ゲルツ編（編）。Einführung in die Kunstliche Intelligenz。アディソン・ウェスリー。 223–263ページ。

• Christoph Walther (1988)。「自動終了証明の基礎としての引数制限アルゴリズム」。第 9 回自動演繹会議議事録。LNAI 。第 310 巻。Springer。pp. 602–621。
• クリストフ・ヴァルサー (1991)。 「自動化フォン・ターミニエルングスベヴァイゼン」。ヴォルフガング・ビーベル編著。Kunstliche Intelligenz。見るeg。 1–254ページ。土井：10.1007/978-3-322-85404-9。ISBN 978-3-528-04771-9。
• クリストフ・ヴァルター（1991年）。「機械によるアルゴリズムの停止性の証明について」人工知能70 （1）。
• Jürgen Giesl、Christoph Walther、Jürgen Brauburger (1998)。「関数型プログラムの終了分析」。Wolfgang Bibel、Peter Schmitt (編) 。自動演繹-アプリケーションの基礎。応用論理シリーズ。第 10 巻。ドルドレヒト: Kluwer Academic Publishers。pp. 135–164。doi :10.1007/978-94-017-0437-3_6。ISBN 978-90-481-5052-6。
• Christoph Walther (2000)。「終了基準」。S. Hölldobler (編)。Intellectics and Computational Logic。ドルドレヒト: Kluwer Academic Publishers。pp. 361–386。
• Christoph Walther、Stephan Schweitzer (2005)。「不完全に定義されたプログラムの自動終了分析」。Franz Baader、Andrei Voronkov (編)。Proc . 11th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR)。LNAI。Vol. 3452。Springer。pp. 332–346。

• Christoph Walther および Stephan Schweitzer (2003)。「VeriFun について」。Franz Baader (編)。Proc . 19th Conference on Automated Deduction。LNAI。Vol . 2741。Springer。pp. 322–327。
• Christoph Walther 、 Stephan Schweitzer (2004)。「教室での検証」。Journal of Automated Reasoning。31 (1): 35–73。doi : 10.1016 /0004-3702(85)90029-3。
• Christoph Walther、Stephan Schweitzer (2005)。「マシン検証コードジェネレータ」。Moshe Y. Vardi、Andrei Voronkov (編)。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)。「不完全に定義されたプログラムに関する推論」。Geoff Sutcliffe、Andrei Voronkov (編)。Proc . 12th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-12)。LNAI。Vol. 3835。Springer。pp. 427–442。
• マルクス・アダーホールド;クリストフ・ヴァルサー;ダニエル・ザリーズ;アンドレアス・シュロッサー (2006)。 「VeriFunの迅速な反証者」。ヴォルフガング・アーレントでは。ピーター・バウムガルトナー;ハンス・ド・ニヴェル (編)。手順非定理、非妥当性、非証明性に関するワークショップ (DISPROVING-06)。 59–69ページ。
• Andreas Schlosser、Christoph Walther、Markus Aderhold (2006)。「VeriFun の公理的仕様」Serge Autexier、Heiko Mantel (編)。第 6 回検証ワークショップ (VERIFY-06) 論文集。pp. 146–163。
• Andreas Schlosser、Christoph Walther、Michael Gonder、 Markus Aderhold (2007)。「VeriFun のコンテキスト依存プロシージャと計算型」。電子理論計算機科学ノート。174 (7): 61–78。doi :10.1016/j.entcs.2006.10.038 。
• Christoph Walther、Nathan Wasser (2017)。「フェルマー、オイラー、ウィルソン - 数論における3つのケーススタディ」。Journal of Automated Reasoning。59 ( 2): 267–286。doi : 10.1007 /s10817-016-9387-z。
• Christoph Walther (2018)。「形式的に検証されたモンゴメリ乗算」。Hana Chockler、Georg Weissenbacher (編)。第30回コンピュータ支援検証インターン会議議事録(CAV 2018)。LNAI。第10982巻。Springer。pp. 505–522。doi :10.1007/ 978-3-319-96142-2_30。ISBN 978-3-319-96141-5。
• Christoph Walther (2019)。「任意の基数のべき乗を法とする乗法逆数に対する検証済みニュートン・ラプソン反復法」。ACM Transactions on Mathematical Software。45 ( 1 ) : 9 :1–9:7。doi :10.1145/3301317。

• Christoph Walther (1983)。「解像度とパラモジュレーションに基づく多ソート計算」。Alan Bundy (編)。第 8 回人工知能インターンシップ合同会議 (IJCAI-8) 議事録。Morgan Kaufmann。pp. 882–891。
• Christoph Walther (1984)。「Schubert の Steamroller の Many-Sorted Resolution による機械的解決」。第 4 回全国人工知能会議 (AAAI-4) 議事録。Morgan Kaufmann。pp. 330–334。
• Christoph Walther (1984)。「多分類理論の統一」。Tim O'Shea (編)。第 6 回ヨーロッパ人工知能会議 (ECAI-6) 議事録。北ホラント。pp. 383–392。
• Walther, Christoph (1985). 「Schubert の Steamroller の Many-Sorted Resolution による機械的解決」Artif. Intell . 26 (2): 217–224. doi :10.1016/0004-3702(85)90029-3.
• Christoph Walther (1986)。「多ソート統合問題の分類」。Jörg Siekmann (編)。第 8 回自動演繹に関する国際会議 (CADE-8) の議事録。LNAI。第 230 巻。Springer。pp. 525–537。
• Christoph Walther (1987)。「解像度とパラモジュレーションに基づく多ソート計算」。Pitman (ロンドン) と Morgan Kaufmann (ロスアルトス)。pp. 1–170。ISBN 978-0-273-08718-2。
• Christoph Walther (1988). 「Many-Sorted Unification」J. ACM . 35 (1): 1–17. doi :10.1145/42267.45071.
• Christoph Walther (1990)。「自動定理証明における多ソート推論」。K.-H. Bläsius、U. Hedtstück、C.-R. Rollinger (編)。人工知能におけるソートとタイプ。LNAI。第 418 巻。Springer。pp. 18–48。
• Christoph Walther (2016). Many-Sorted Unification のアルゴリズム (Many-Sorted Unification の正誤表、J. ACM vol 35(1)、1988) (技術レポート)。TU Darmstadt。

• Susanne Biundo、Birgit Hummel、Dieter Hutter、Christoph Walther (1986)。「カールスルーエ誘導定理証明システム」。JH Siekmann (編)。Proc . 8th CADE . LNAI. Vol. 230. Springer. pp. 672–674。
• Christoph Walther (1992)。「数学的帰納法」。SC Shapiro (編) 著。人工知能百科事典。John Wiley and Sons。pp. 668–672。
• クリストフ・ヴァルサー (1992)。 「コンピューティング帰納法公理」(PDF)。アンドレイ・ヴォロンコフ（編）。手順LPAR。 LNAI。 Vol. 624.スプリンガー。 381–392ページ。
• クリストフ・ヴァルサー (1993)。 「機械による帰納公理の結合」(PDF)。 Ruzena Bajcsy (編)。手順第13回IJCAI。モーガン・カウフマン。 95–101ページ。
• Christoph Walther (1994)。「数学的帰納法」(PDF)。Dov M. Gabbay、CJ Hogger、JA Robinson (編)。 『人工知能と論理プログラミングにおける論理ハンドブック』第 2 巻。オックスフォード大学出版局。pp. 127–227。
• クリストフ・ヴァルサー (2001)。 「セマンティックとプログラムの検証」。Teubner Texte zur Informatik。 TEUBNER-TEXTE zur Informatik。 Vol. 34. トイブナー・ワイリー。 1–212ページ。土井：10.1007/978-3-322-86768-1。ISBN 978-3-519-00336-6。

• ダルムシュタット大学のクリストフ・ヴァルターのホームページ
• ダルムシュタット大学の VeriFun システム