Deepak Kapur

Deepak Kapur
Född	( 1950-08-24 ) 24 augusti 1950 Amritsar, Punjab, Indien
Nationalitet	Indisk, amerikansk
Alma mater	Indian Institute of Technology Kanpur Massachusetts Institute of Technology
Make	Roli Varma
Barn	Ila Kapur Varma
Utmärkelser	Herbrand Award (2009)
Vetenskaplig karriär
Fält	Automatiserade resonemang , termomskrivning , enande , symbolisk beräkning , formella metoder
Avhandling	Mot en teori om abstrakta datatyper. (1980)
Doktorand rådgivare	Barbara Liskov
Hemsida	https://www.cs.unm.edu/~kapur/

Deepak Kapur (född 24 augusti 1950) är en framstående professor vid avdelningen för datavetenskap vid University of New Mexico .

Biografi

Kapur föddes i en lägre medelklassfamilj baserad i Amritsar , där hans far, Nawal Kishore Kapur, var en tygmäklare; hans mor, Bimla Vati, var hemmafru.

Utbildning

Kapurs tidiga utbildning var på Government Primary School, Katra Khazana, Amritsar, fram till 3:e klass. Han flyttades sedan till Vidya Bhushan Primary School, Amritsar. Efter 5:e klass var han tvungen att byta skola igen till Dayanand Anglo Vedic (DAV) Higher Secondary School fram till 11:e klass. Han valdes i Indian Institute of Technology (IIT) inträdesprov 1966. Han tog sin grundexamen (B.Tech) i elektroteknik från IIT, Kanpur, 1971 och M. Tech. examen i datavetenskap i maj 1973 också från IIT, Kanpur.

Akademisk karriär

Efter examen från MIT i mars 1980, började Kapur som forskarstab vid GE Corporate Research and Development (GECRD), Schenectady, NY, där han arbetade fram till december 1987. Samtidigt som han var på GECRD var han adjungerad professor vid Rensselaer Polytechnic Institute (RPI), där han undervisade i en kurs i automatiserat resonemang baserat på termomskrivning. På RPI var han också medhandledare för Ph.D. avhandlingar av Abdelilah Kandri-Rody och Hantao Zhang.

Kapur anställdes 1988 som fast professor vid University i Albany, State University of New York. 1998 fick Kapur det förnämliga forskningspriset.

Kapur blev ordförande för datavetenskapsavdelningen vid University of New Mexico (UNM) i december 1998, en position han innehade fram till juni 2006. 2007 utnämndes Kapur till en framstående professor vid UNM. I maj 2010 tilldelades Kapur Senior Faculty Research Excellence Award av School of Engineering vid UNM.

Kapur har haft besöksutnämningar vid Massachusetts Institute of Technology , Max Planck Institute for Informatics , Tata Institute of Fundamental Research, Mumbai, Indian Institute of Technology, Delhi , Institute of Software (Peking), Chinese Academy of Sciences (ISCAS), Institutet IMDEA Programvara, Madrid, bland andra institutioner.

Kapur har fungerat som konsult för GE Corporate Research and Development, Sandia National Labs, IBM Research på Watson och Fujitsu Labs.

Kapur var chefredaktör för Journal of Automated Reasoning 1993-2007. Han har suttit i redaktionen för många tidskrifter, inklusive Journal of Automated Reasoning , Journal of Symbolic Computation , Journal of Logic and Algebra Programming, Journal of Applicable Algebra in Engineering, Communication and Computing. Kapur satt också i styrelsen för Leibniz International Proceedings in Informatics.

Kapur var styrelseledamot vid United Nations University - International Institute for Software Technology samt United Nation University - Computing and Society. Han var också styrelseledamot i Computer Science Research Institute vid Sandia National Laboratories och Los Alamos Computer Science Institute (LACSI).

Kapur fick Herbrand Award 2009:

som ett erkännande för hans framstående bidrag till flera områden av automatiserad deduktion, inklusive bevisning av induktiv sats, bevisning av geometrisats, termomskrivning, unifieringsteori, integration och kombination av beslutsförfaranden, generering av lemma och slinginvariant, såväl som hans arbete med datoralgebra, som hjälpte till att överbrygga klyftan mellan de två områdena.

Forskning

Kapur har publicerat över 150 artiklar om programmeringsspråk, formella metoder inklusive mjukvaru- och hårdvaruverifiering, automatiserad satsprovning, termomskrivning, induktiv satsbevisning, unifieringsteori, komplexitet hos automatiserade resonemangsalgoritmer, geometrisatsbevisande, Groebner-bas, parametrisk (Grovebnerive) Basis, Multivariate Dixon Resultants, bland andra ämnen.

Kapur utvecklade mjukvaruverktyget Rewrite Rule Laboratory (RRL), världens första teorembevis baserat på termomskrivning och Knuth-Bendix-kompletteringsproceduren och dess generalisering. Satsbeviset mekaniserade ekvationellt, första ordningens och induktivt resonemang. På GECRD designade och ledde Kapur utvecklingen av GeoMeter, ett system för geometriska och algebraiska resonemang baserat på Groebner-bas och parametrisk Groebner-bas för tillämpningar för geometrisatsbevisande och datorseende. Vid universitetet i Albany, State University of New York, ledde Kapur tillsammans med Musser utvecklingen av ett hypertextbaserat system, Tecton, för hierarkisk bevishantering., utöver RRL. Dessa system har använts i tillämpningar av hårdvaruverifiering, specifikationsanalys, geometrisk modellering och datorseende.

Utvalda publikationer

•   Donald, BR; Kapur, D.; Mundy, JL (1992). Symbolisk och numerisk beräkning för artificiell intelligens . Akademisk press. ISBN 978-0-12-220535-4 .

• Kapur, D.; Mundy, JL Geometriskt resonemang | MIT Press . mitpress.mit.edu . MIT Tryck på . Hämtad 2021-06-06 .

•   Varma, R.; Kapur, D. (23 april 2015). "Avkoda femininitet i datavetenskap i Indien". Kommunikation från ACM . 58 (5): 56–62. doi : 10.1145/2663339 . S2CID 18503653 .

•   Varma, R.; Kapur, D. (augusti 2013). "Jämförande analys av hjärnflykt, hjärncirkulation och hjärnhållning: en fallstudie av indiska tekniska institut". Journal of Comparative Policy Analysis: Research and Practice . 15 (4): 315–330. doi : 10.1080/13876988.2013.810376 . S2CID 41370320 .

•   Kapur, D.; Zhang, H. (1995-01-01). "En översikt över Rewrite Rule Laboratory (RRL)" . Datorer och matematik med applikationer . 29 (2): 91–114. doi : 10.1016/0898-1221(94)00218-A . ISSN 0898-1221 .

• Kapur, D.; Nie, X.; Musser, DR (oktober 1994). "En översikt över Tecton proof-systemet" . Teoretisk datavetenskap . 133 (2): 307–339. doi : 10.1016/0304-3975(94)90192-9 .

•   Kapur, D.; Musser, DR (1987-02-01). "Bevis genom konsekvens" . Artificiell intelligens . 31 (2): 125–157. doi : 10.1016/0004-3702(87)90017-8 . ISSN 0004-3702 .

•   Kapur, D.; Giesl, J.; Subramaniam, M. (2004). "Introduktions- och beslutsförfaranden". Rev.R. Acad. Cien. Serie A. Mat . CiteSeerX 10.1.1.70.2434 .

•   Zhang, H.; Kapur, D.; Krishnamoorthy, MS (1988-05-23). "En mekaniserbar induktionsprincip för ekvationella specifikationer" . 9:e internationella konferensen om automatiskt avdrag . Föreläsningsanteckningar i datavetenskap. Springer, Berlin, Heidelberg. 310 : 162–181. doi : 10.1007/BFb0012831 . ISBN 3-540-19343-X .

• Kapur, Deepak; Narendran, Paliath (18 augusti 1985). "En ekvationell metod för att teorem bevisar i första ordningens predikatkalkyl" . Handlingar från den nionde internationella gemensamma konferensen om artificiell intelligens - volym 2 . Morgan Kaufmann Publishers Inc.: 1146–1153.

•    Kandri-Rody, A.; Kapur, D.; Winkler, F. (1989). "Knuth-Bendix-förfarande och Buchberger-algoritm: en syntes". Proceedings of ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation - ISSAC '89 : 55–67. doi : 10.1145/74540.74548 . ISBN 0897913256 . S2CID 17914831 .

•   Kandri-Rody, Ä.; Kapur, D. (1 augusti 1988). "Beräkning av en Grobner-bas för ett polynomideal över en euklidisk domän" . Journal of Symbolic Computation . 6 (1): 37–57. doi : 10.1016/S0747-7171(88)80020-8 . ISSN 0747-7171 .

•   Kapur, D. (1986-12-01). "Att använda Gröbner-baser för att resonera kring geometriproblem" . Journal of Symbolic Computation . 2 (4): 399-408. doi : 10.1016/S0747-7171(86)80007-4 . ISSN 0747-7171 .

•   Kapur, D.; Mundy, J. (1 december 1988). "Wus metod och dess tillämpning på perspektivvisning" . Artificiell intelligens . 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). "Lösa polynomsystem med hjälp av en gren- och beskärningsmetod" . SIAM Journal on Numerical Analysis . 34 (2): 797–827. doi : 10.1137/S0036142995281504 . ISSN 0036-1429 .

•   Kapur, D. (1993). "En metod för att lösa system av parametriska polynomekvationer i". Principer och praxis för begränsningsprogrammering . CiteSeerX 10.1.1.39.9091 .

•   Kapur, D. (februari 2017). "Omfattande Gröbner grundteori för ett parametriskt polynomideal och den tillhörande kompletteringsalgoritmen". Journal of Systems Science and Complexity . 30 (1): 196–233. doi : 10.1007/s11424-017-6337-8 . S2CID 33584098 .

•   Michel, JD; Nandhakumar, N.; Saxena, T.; Kapur, D. (1 oktober 1998). "Geometriska, algebraiska och termofysiska tekniker för objektigenkänning i IR-bilder" . Datorseende och bildförståelse . 72 (1): 84–97. doi : 10.1006/cviu.1997.0669 . ISSN 1077-3142 .

•   Kapur, D.; Madlener, K. (1989). "En kompletteringsprocedur för att beräkna en kanonisk grund för en k-subalgebra" . Datorer och matematik : 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). "Algebraiska och geometriska resonemang med hjälp av Dixon-resultanter" . Proceedings of the International Symposium on Symbolic and Algebraic Computation . ISSAC '94. Oxford, Storbritannien: Association for Computing Machinery: 99–107. doi : 10.1145/190347.190372 . ISBN 978-0-89791-638-7 . S2CID 6398360 .

•   Chtcherba, A.; Kapur, D. (1 juli 2004). "Konstruera resulterande matriser av Sylvester-typ med användning av Dixon-formuleringen" . Journal of Symbolic Computation . 38 (1): 777–814. doi : 10.1016/j.jsc.2003.11.003 . ISSN 0747-7171 .

• Chtcherba, AD; Kapur, D. (september 2003). "Exakta resultat för hörnskurna oblandade multivariata polynomsystem med hjälp av Dixon-formuleringen" . Journal of Symbolic Computation . 36 (3–4): 289–315. doi : 10.1016/S0747-7171(03)00084-1 .

•   Kapur, D.; Subramaniam, M. (september 2000). "Att använda en induktionsprovare för att verifiera aritmetiska kretsar". International Journal on Software Tools for Technology Transfer . 3 (1): 32–65. doi : 10.1007/PL00010808 . S2CID 10544549 .

•   Falke, S.; Kapur, D. (2015). "När är en formel en slinga invariant?". Logik, omskrivning och samtidighet . Föreläsningsanteckningar i datavetenskap. 9200 : 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). "Genererar alla polynominvarianter i enkla slingor" . Journal of Symbolic Computation . 42 (4): 443–476. doi : 10.1016/j.jsc.2007.01.002 . ISSN 0747-7171 .

• Kapur, D. (2006). Baader, Franz; Baumgartner, Peter; Nieuwenhuis, Robert; Voronkov, Andrei (red.). "Automatiskt generera loopinvarianter med hjälp av kvantifierareliminering" . Avdrag och ansökningar . Dagstuhl Seminarium Proceedings. Dagstuhl, Tyskland: Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Tyskland.

•   Kapur, D. (2013). "Elimineringstekniker för programanalys". Programmeringslogik . Föreläsningsanteckningar i datavetenskap. 7797 : 194–215. doi : 10.1007/978-3-642-37651-1_8 . ISBN 978-3-642-37650-4 .

•    Kapur, D.; Majumdar, R.; Zarba, CG (2006). "Interpolation för datastrukturer". Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering - SIGSOFT '06/FSE-14 : 105. doi : 10.1145/1181775.1181789 . ISBN 1595934685 . S2CID 158878 .

• Ghilardi, S.; Gianola, A.; Kapur, D. (2020). "Computing Uniform Interpolants for EUF via (villkorliga) DAG-baserade Compact Representations" . Italiensk konferens om beräkningslogik : 67–81.

•    Kapur, D.; Narendran, P. (1992-10-01). "Komplexiteten av föreningsproblem med associativ-kommutativa operatorer" . 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). "Komplexiteten i matchningsproblem" . Journal of Symbolic Computation . 3 (1–2): 203–216. doi : 10.1016/S0747-7171(87)80027-5 . ISSN 0747-7171 .

•   Kapur, D.; Musser, D.; Narendran, P.; Stillman, J. (1991). "Halvförening". Tidskrift för teoretisk datavetenskap . 81 (2): 169–187. CiteSeerX 10.1.1.90.1272 . doi : 10.1016/0304-3975(91)90189-9 .