ディーパック・カプール

ディーパック・カプール（1950年8月24日生まれ）は、ニューメキシコ大学コンピュータサイエンス学部の特別教授である。^[3]

カプールはアムリトサルの下層中流階級の家庭に生まれた。父親のナワル・キショア・カプールは布地仲買人、母親のビムラ・ヴァティは主婦だった。^[要出典]

カプールは、アムリトサルのカトラ・カザナ公立小学校で3年生まで教育を受け、その後、アムリトサルのヴィディヤ・ブーシャン小学校に転校した。5年生の後、11年生までダヤナンド・アングロ・ヴェーダ（DAV）高等中学校に転校しなければならなかった。^{[要出典] 1966年に}インド工科大学（IIT）の入学試験に合格。1971年にインド工科大学カンプール校で電気工学の学士号（B.Tech）を取得し、1973年5月に同じくインド工科大学カンプール校でコンピューターサイエンスの修士号を取得した。

1980 年 3 月に MIT を卒業した後、Kapur はニューヨーク州スケネクタディの GE Corporate Research and Development (GECRD) に研究員として入社し、1987 年 12 月まで勤務しました。GECRD 在籍中、彼は Rensselaer Polytechnic Institute (RPI) の非常勤教授として、用語書き換えに基づく自動推論のコースを教えていました。RPI では、Abdelilah Kandri-Rody と Hantao Zhang の博士論文の共同指導も行いました。

カプール氏は1988年にニューヨーク州立大学アルバニー校の終身在職権を持つ教授として採用された。1998年にカプール氏は優秀研究賞を受賞した。

カプール氏は 1998 年 12 月にニューメキシコ大学 (UNM) のコンピューター サイエンス学部の学部長に就任し、2006 年 6 月までその職を務めました。2007 年には、カプール氏は UNM の特別教授に任命されました。2010 年 5 月には、カプール氏はUNM の工学部から 上級教員研究優秀賞を受賞しました。

カプール氏は、マサチューセッツ工科大学、マックス・プランク情報科学研究所、ムンバイのタタ基礎研究所、デリーのインド工科大学、北京ソフトウェア研究所、中国科学院（ISCAS）、マドリードのIMDEAソフトウェア研究所など、さまざまな機関で 客員研究員を務めてきました。

Kapur 氏は、GE コーポレート研究開発、サンディア国立研究所、IBM ワトソン研究所、富士通研究所のコンサルタントを務めてきました。

Kapur 氏は、1993 年から 2007 年までJournal of Automated Reasoningの編集長を務めました。また、Journal of Automated Reasoning、Journal of Symbolic Computation、Journal of Logic and Algebra Programming、Journal of Applicable Algebra in Engineering, Communication and Computing など、多数のジャーナルの編集委員を務めました。Kapur 氏はまた、Leibniz International Proceedings in Informatics の委員も務めました。

カプール氏は、国連大学国際ソフトウェア技術研究所および国連大学コンピューティングと社会研究所の理事を務めていました。また、サンディア国立研究所のコンピュータサイエンス研究所およびロスアラモスコンピュータサイエンス研究所 (LACSI) の理事も務めました。

カプールは2009年にヘルブラン賞を受賞した。^[4]

帰納的定理証明、幾何学定理証明、項書き換え、統一理論、決定手続きの積分と組み合わせ、補題とループ不変式の生成など、自動演繹のいくつかの分野への彼の独創的な貢献、および2つの分野間のギャップを埋めるのに役立ったコンピュータ代数の研究が認められて。

カプールは、プログラミング言語、ソフトウェアとハ​​ードウェアの検証を含む形式手法、自動定理証明、項書き換え、帰納的定理証明、統一理論、自動推論アルゴリズムの複雑性、幾何学定理証明、グレブナー基底、パラメトリック（包括的）グレブナー基底、多変量ディクソン結果など、さまざまなトピックについて150を超える論文を発表しています。^[5]

Kapur は、項書き換えと Knuth-Bendix 完備化手順およびその一般化に基づく世界初の定理証明器であるソフトウェア ツール Rewrite Rule Laboratory (RRL) を開発した。^[6]この定理証明器は、等式、一次、および帰納的推論を機械化した。GECRD では、Kapur は、幾何学定理証明とコンピューター ビジョンへの応用を目的とした、グレブナー基底とパラメトリック グレブナー基底に基づく幾何学および代数推論システムである GeoMeter を設計し、その開発を主導した。ニューヨーク州立大学アルバニー校では、Kapur は Musser とともに、RRL をベースにした階層的証明管理のためのハイパーテキスト ベースのシステム Tecton の開発を主導した。^[7]これらのシステムは、ハードウェア検証、仕様分析、幾何学モデリング、およびコンピューター ビジョンのアプリケーションで使用されている。

• ドナルド、BR; カプール、D.; マンディ、JL (1992)。人工知能のための記号計算と数値計算。アカデミック プレス。ISBN 978-0-12-220535-4。
• Kapur, D.; Mundy, JL 幾何学的推論 | The MIT Press. MIT Press . 2021-06-06に取得。 {{cite book}}:|website=無視されました (ヘルプ)
• Varma, R.; Kapur , D. (2015 年4月23日)。「インドのコンピュータ サイエンスにおける女性らしさの解読」Communications of the ACM。58 ( 5): 56–62。doi :10.1145/2663339。S2CID  18503653。
• Varma, R.; Kapur, D. (2013 年 8 月)。「頭脳流出、頭脳循環、頭脳保持の比較分析: インド工科大学の事例研究」。比較政策分析ジャーナル: 研究と実践。15 ( 4): 315–330。doi :10.1080/13876988.2013.810376。S2CID 41370320  。
• Kapur, D.; Zhang, H. (1995-01-01). 「Rewrite Rule Laboratory (RRL) の概要」. Computers & Mathematics with Applications . 29 (2): 91–114. doi :10.1016/0898-1221(94)00218-A. ISSN  0898-1221.
• Kapur, D.; Nie, X.; Musser, DR (1994 年 10 月). 「Tecton 証明システムの概要」.理論計算機科学. 133 (2): 307–339. doi : 10.1016/0304-3975(94)90192-9 .
• Kapur, D.; Musser, DR (1987-02-01). 「一貫性による証明」.人工知能. 31 (2): 125–157. doi :10.1016/0004-3702(87)90017-8. ISSN  0004-3702.
• カプール、D.ギースル、J.スブラマニアム、M. (2004)。 「誘導と決定の手順」。Rev.R.アカド。シエン。セリエA.マット。CiteSeerX  10.1.1.70.2434。
• Zhang, H.; Kapur, D.; Krishnamoorthy, MS (1988-05-23)。「等式仕様のための機械化可能な帰納原理」。第9 回自動演繹国際会議。コンピュータ サイエンスの講義ノート。第 310 巻。Springer、ベルリン、ハイデルベルク。pp. 162–181。doi : 10.1007/BFb0012831。ISBN 3-540-19343-X。
• Kapur, Deepak; Narendran, Paliath (1985 年 8 月 18 日)。「一階述語計算における定理証明への等式アプローチ」。人工知能に関する第 9 回国際合同会議議事録 - 第 2 巻。Morgan Kaufmann Publishers Inc.: 1146–1153。
• Kandri-Rody, A.; Kapur, D.; Winkler, F. (1989). 「Knuth-Bendix 手順と Buchberger アルゴリズム: 統合」。ACM -SIGSAM 1989 国際シンポジウム「記号および代数計算 - ISSAC '89」の議事録。pp . 55–67。doi :10.1145/ 74540.74548。ISBN 0897913256. S2CID  17914831。
• Kandri-Rody, Ä.; Kapur, D. (1988 年 8 月 1 日). 「ユークリッド領域上の多項式イデアルの Grobner 基底の計算」. Journal of Symbolic Computation . 6 (1): 37–57. doi :10.1016/S0747-7171(88)80020-8. ISSN  0747-7171.
• Kapur, D. (1986-12-01). 「グレブナー基底を用いた幾何学問題の推論」Journal of Symbolic Computation . 2 (4): 399–408. doi :10.1016/S0747-7171(86)80007-4. ISSN  0747-7171.
• Kapur, D.; Mundy, J. (1988 年 12 月 1 日). 「Wu 法と透視図法への応用」.人工知能. 37 (1–3): 15–36. doi :10.1016/0004-3702(88)90048-3. ISSN  0004-3702.
• Van Hentenryck, P.; McAllester, D.; Kapur, D. (1997-04-01). 「分岐とプルーン法を用いた多項式システムの解法」. SIAM Journal on Numerical Analysis . 34 (2): 797–827. doi :10.1137/S0036142995281504. ISSN  0036-1429.
• Kapur, D. (1993)。「パラメトリック多項式方程式のシステムを解くためのアプローチ」制約プログラミングの原則と実践。CiteSeerX 10.1.1.39.9091 。
• Kapur, D. (2017 年 2 月)。「パラメトリック多項式イデアルの包括的なグレブナー基底理論とそれに関連する補完アルゴリズム」。システム科学と複雑性ジャーナル。30 (1): 196–233。doi : 10.1007 /s11424-017-6337-8。S2CID 33584098  。
• Michel, JD; Nandhakumar, N.; Saxena, T.; Kapur, D. (1998 年 10 月 1 日)。「IR 画像における物体認識のための幾何学的、代数的、および熱物理的手法」。コンピュータビジョンと画像理解。72 (1): 84–97。doi :10.1006/ cviu.1997.0669。ISSN 1077-3142  。
• Kapur, D.; Madlener, K. (1989). 「k-部分代数の標準基底を計算するための完了手順」.コンピュータと数学. pp. 1–11. doi :10.1007/978-1-4613-9647-5_1. ISBN 978-0-387-97019-6。
• Kapur, D.; Saxena, T.; Yang, L. (1994-08-01). 「Dixon の結果を用いた代数的および幾何学的推論」。記号および代数的計算に関する国際シンポジウム - ISSAC '94 の議事録。オックスフォード、イギリス: 計算機協会。pp. 99–107。doi : 10.1145 /190347.190372。ISBN 978-0-89791-638-7. S2CID  6398360。
• Chtcherba, A.; Kapur, D. (2004 年 7 月 1 日). 「Dixon 定式化を使用したシルベスター型結果行列の構築」. Journal of Symbolic Computation . 38 (1): 777–814. doi : 10.1016/j.jsc.2003.11.003 . ISSN  0747-7171.
• Chtcherba, AD; Kapur, D. (2003 年 9 月). 「Dixon 定式化を使用したコーナーカット非混合多変数多項式システムの正確な結果」. Journal of Symbolic Computation . 36 (3–4): 289–315. doi : 10.1016/S0747-7171(03)00084-1 .
• Kapur, D.; Subramaniam, M. ( 2000 年 9 月)。「算術回路の検証に誘導証明器を使用する」。技術移転のためのソフトウェア ツールに関する国際ジャーナル。3 ( 1): 32–65。doi : 10.1007 /PL00010808。S2CID  10544549。
• Falke, S.; Kapur, D. (2015)。「式がループ不変となるのはいつですか?」。論理、書き換え、並行性。コンピュータサイエンスの講義ノート。第 9200 巻。pp. 264–286。doi : 10.1007 / 978-3-319-23165-5_13。ISBN 978-3-319-23164-8。
• Rodriguez-Carbonell, E.; Kapur, D. (2007-04-01). 「単純なループですべての多項式不変量を生成する」Journal of Symbolic Computation . 42 (4): 443–476. doi : 10.1016/j.jsc.2007.01.002 . ISSN  0747-7171.
• カプール、D. (2006)。バーダー、フランツ。バウムガルトナー、ピーター。ニーウェンハウス、ロバート。ヴォロンコフ、アンドレイ（編）。 「量指定子の消去を使用したループ不変条件の自動生成」。控除と申請。ダグシュトゥール セミナー議事録。ダグシュトゥール、ドイツ: Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI)、シュロス ダグシュトゥール、ドイツ。
• Kapur, D. (2013). 「プログラム分析のための消去法」。プログラミング ロジック。コンピュータ サイエンスの講義ノート。第 7797 巻。pp. 194–215。doi : 10.1007 / 978-3-642-37651-1_8。ISBN 978-3-642-37650-4。
• Kapur, D.; Majumdar, R.; Zarba, CG (2006)。「データ構造の補間」。ソフトウェア エンジニアリングの基礎に関する第 14 回 ACM SIGSOFT 国際シンポジウムの議事録。pp. 105–116。doi : 10.1145 / 1181775.1181789。ISBN 1595934685.S2CID 158878  。
• Ghilardi, S.; Gianola, A.; Kapur, D. (2020). 「(条件付き) DAG ベースのコンパクト表現による EUF の均一補間の計算」。イタリア計算論理会議: 67–81。
• Kapur, D.; Narendran, P. (1992-10-01). 「結合可換演算子による統一問題の複雑さ」. Journal of Automated Reasoning . 9 (2): 261–288. doi :10.1007/BF00245463. ISSN  1573-0670. S2CID  26828762.
• Benanav, D.; Kapur, D.; Narendran, P. (1987-02-04). 「マッチング問題の複雑さ」Journal of Symbolic Computation . 3 (1–2): 203–216. doi :10.1016/S0747-7171(87)80027-5. ISSN  0747-7171.
• カプール、D.マッサー、D.ナレンドラン、P.スティルマン、J. (1991)。 「半統一」。理論コンピュータサイエンスのジャーナル。81 (2): 169–187。CiteSeerX  10.1.1.90.1272。土井：10.1016/0304-3975(91)90189-9。