Deepak Kapur Explained
Deepak Kapur (born August 24, 1950) is a Distinguished Professor in the Department of Computer Science at the University of New Mexico.[2]
Biography
Kapur was born in a lower-middle-class family based in Amritsar, where his father, Nawal Kishore Kapur, was a cloth broker; his mother, Bimla Vati, was a housewife.
Education
Kapur's early education was at the Government Primary School, Katra Khazana, Amritsar, until 3rd grade. He was then shifted to the Vidya Bhushan Primary School, Amritsar. After 5th grade, he had to change school again to Dayanand Anglo Vedic (DAV) Higher Secondary School until 11th grade. He was selected in the Indian Institute of Technology (IIT) entrance examination in 1966. He got his undergraduate degree (B.Tech) in Electric Engineering from IIT, Kanpur, in 1971 and M. Tech. degree in Computer Science in May 1973 also from IIT, Kanpur.
Academic career
After graduating from MIT in March 1980, Kapur joined as a research staff at GE Corporate Research and Development (GECRD), Schenectady, NY, where he worked until Dec. 1987. While being at GECRD, he was an adjunct professor at Rensselaer Polytechnic Institute (RPI), where he taught a course on automated reasoning based on term rewriting. At RPI he also co-supervised Ph.D. dissertations of Abdelilah Kandri-Rody and Hantao Zhang.
Kapur was hired in 1988 as a tenured full professor at the University at Albany, State University of New York. In 1998, Kapur got the distinguished research award.
Kapur became the Chair of the Computer Science department at the University of New Mexico (UNM) in December 1998, a position he held until June 2006. In 2007, Kapur was made a Distinguished Professor at UNM. In May, 2010, Kapur was awarded Senior Faculty Research Excellence Award by the School of Engineering of the UNM.
Kapur has held visiting appointments at Massachusetts Institute of Technology, Max Planck Institute for Informatics, Tata Institute of Fundamental Research, Mumbai, Indian Institute of Technology, Delhi, Institute of Software (Beijing), the Chinese Academy of Sciences (ISCAS), Institute IMDEA Software, Madrid, among other institutions.
Kapur has served as a Consultant to GE Corporate Research and Development, Sandia National Labs, IBM Research at Watson and Fujitsu Labs.
Kapur was the Editor-in-Chief of the Journal of Automated Reasoning from 1993-2007. He has served on the editorial board of many journals including Journal of Automated Reasoning, Journal of Symbolic Computation, Journal of Logic and Algebra Programming, Journal of Applicable Algebra in Engineering, Communication and Computing. Kapur also served on the board of Leibniz International Proceedings in Informatics.
Kapur was a Board Member of the United Nations University - International Institute for Software Technology as well as United Nation University - Computing and Society. He was also a board member of the Computer Science Research Institute of the Sandia National Laboratories and Los Alamos Computer Science Institute (LACSI).
Kapur received the Herbrand Award in 2009:[3]
Research
Kapur has published over 150 papers on Programming Languages, Formal Methods including Software and Hardware Verification, Automated Theorem Proving, Term Rewriting, Inductive Theorem Proving, Unification Theory, Complexity of Automated Reasoning Algorithms, Geometry Theorem Proving, Groebner basis, parametric (Comprehensive) Groebner Basis, Multivariate Dixon Resultants, among other topics.[4]
Kapur developed the software tool Rewrite Rule Laboratory (RRL), the world’s first theorem prover based on term rewriting and the Knuth-Bendix completion procedure and its generalization.[5] The theorem prover mechanized equational, first-order, and inductive reasoning. At GECRD, Kapur designed and led the development of GeoMeter, a system for geometric and algebraic reasoning based on Groebner basis and parametric Groebner basis for applications to geometry theorem proving and computer vision.At the University at Albany, State University of New York, Kapur with Musser led the development of a hypertext based system, Tecton, for hierarchical proof management.,[6] on top of RRL.These systems have been used in applications of hardware verification, specification analysis, geometric modeling, and computer vision.
Selected publications
- Book: Donald. B.R.. Symbolic and Numerical Computation for Artificial Intelligence. Kapur. D.. Mundy. J.L.. 1992. Academic Press. 978-0-12-220535-4. en.
- Book: Kapur. D.. Mundy. J.L.. Geometric Reasoning The MIT Press. 2021-06-06. mitpress.mit.edu. MIT Press. en.
- Varma . R.. Kapur . D.. Decoding femininity in computer science in India . Communications of the ACM . 23 April 2015 . 58 . 5 . 56–62 . 10.1145/2663339. 18503653.
- Varma . R.. Kapur . D.. Comparative Analysis of Brain Drain, Brain Circulation and Brain Retain: A Case Study of Indian Institutes of Technology . Journal of Comparative Policy Analysis: Research and Practice . August 2013 . 15 . 4 . 315–330 . 10.1080/13876988.2013.810376. 41370320.
- Kapur. D.. Zhang. H.. 1995-01-01. An overview of Rewrite Rule Laboratory (RRL). Computers & Mathematics with Applications. en. 29. 2. 91–114. 10.1016/0898-1221(94)00218-A. 0898-1221.
- Kapur . D. . Nie . X. . Musser . D.R. . An overview of the Tecton proof system . Theoretical Computer Science . October 1994 . 133 . 2 . 307–339 . 10.1016/0304-3975(94)90192-9. free .
- Kapur . D. . Musser . D.R. . 1987-02-01 . Proof by consistency. Artificial Intelligence. en. 31. 2. 125–157. 10.1016/0004-3702(87)90017-8. 0004-3702.
- Kapur . D.. Giesl . J.. Subramaniam . M.. Induction and Decision Procedures . Rev.R. Acad. Cien. Serie A. Mat.. 2004 . 10.1.1.70.2434.
- Book: Zhang. H.. Kapur. D.. Krishnamoorthy. M.S.. 9th International Conference on Automated Deduction . A mechanizable induction principle for equational specifications . 1988-05-23. https://link.springer.com/chapter/10.1007/BFb0012831. Lecture Notes in Computer Science. 310. en. Springer, Berlin, Heidelberg. 162–181. 10.1007/BFb0012831. 3-540-19343-X.
- Kapur . Deepak . Narendran . Paliath . An equational approach to theorem proving in first-order predicate calculus . Proceedings of the 9th International Joint Conference on Artificial Intelligence - Volume 2 . 18 August 1985 . 1146–1153 . Morgan Kaufmann Publishers Inc..
- Book: Kandri-Rody. A.. Kapur . D. . Winkler . F. . Proceedings of the ACM-SIGSAM 1989 international symposium on Symbolic and algebraic computation - ISSAC '89 . Knuth-Bendix procedure and Buchberger algorithm: A synthesis . 1989 . 55–67 . 10.1145/74540.74548. 0897913256. 17914831.
- Kandri-Rody . Ä.. Kapur . D.. Computing a Grobner basis of a polynomial ideal over a Euclidean domain . Journal of Symbolic Computation . 1 August 1988 . 6 . 1 . 37–57 . 10.1016/S0747-7171(88)80020-8 . 0747-7171.
- Kapur. D.. 1986-12-01. Using Gröbner bases to reason about geometry problems. Journal of Symbolic Computation. en. 2. 4. 399–408. 10.1016/S0747-7171(86)80007-4. 0747-7171.
- Kapur . D. . Mundy . J. . Wu's method and its application to perspective viewing . Artificial Intelligence . 1 December 1988 . 37 . 1–3 . 15–36 . 10.1016/0004-3702(88)90048-3 . en . 0004-3702.
- Van Hentenryck. P.. McAllester. D.. Kapur. D.. 1997-04-01. Solving Polynomial Systems Using a Branch and Prune Approach. SIAM Journal on Numerical Analysis. 34. 2. 797–827. 10.1137/S0036142995281504. 0036-1429.
- Book: Kapur . D.. Principles and Practices of Constraint Programming . An Approach for Solving Systems of Parametric Polynomial Equations in . 1993 . 10.1.1.39.9091.
- Kapur . D.. Comprehensive Gröbner basis theory for a parametric polynomial ideal and the associated completion algorithm . Journal of Systems Science and Complexity . February 2017 . 30 . 1 . 196–233 . 10.1007/s11424-017-6337-8. 33584098.
- Michel . J.D. . Nandhakumar . N.. Saxena. T.. Kapur . D. . Geometric, Algebraic, and Thermophysical Techniques for Object Recognition in IR Imagery . Computer Vision and Image Understanding . 1 October 1998 . 72 . 1 . 84–97 . 10.1006/cviu.1997.0669 . en . 1077-3142.
- Book: Kapur. D. . Madlener . K.. Computers and Mathematics . A Completion Procedure for Computing a Canonical Basis for a k-Subalgebra . 1989. https://link.springer.com/chapter/10.1007/978-1-4613-9647-5_1. en. 1–11. 10.1007/978-1-4613-9647-5_1. 978-0-387-97019-6.
- Book: Kapur. D.. Saxena. T.. Yang. L.. Proceedings of the international symposium on Symbolic and algebraic computation - ISSAC '94 . Algebraic and geometric reasoning using Dixon resultants . 1994-08-01. Oxford, United Kingdom. Association for Computing Machinery. 99–107. 10.1145/190347.190372. 978-0-89791-638-7. 6398360. free.
- Chtcherba . A. . Kapur . D. . Constructing Sylvester-type resultant matrices using the Dixon formulation . Journal of Symbolic Computation . 1 July 2004 . 38 . 1 . 777–814 . 10.1016/j.jsc.2003.11.003 . en . 0747-7171. free .
- Chtcherba . A.D. . Kapur . D.. Exact resultants for corner-cut unmixed multivariate polynomial systems using the Dixon formulation . Journal of Symbolic Computation . September 2003 . 36 . 3–4 . 289–315 . 10.1016/S0747-7171(03)00084-1. free .
- Kapur . D.. Subramaniam . M.. Using an induction prover for verifying arithmetic circuits . International Journal on Software Tools for Technology Transfer . September 2000 . 3 . 1 . 32–65 . 10.1007/PL00010808. 10544549.
- Book: Falke . S.. Kapur . D.. Logic, Rewriting, and Concurrency . When is a Formula a Loop Invariant? . Lecture Notes in Computer Science. 2015 . 9200 . 264–286 . 10.1007/978-3-319-23165-5_13. 978-3-319-23164-8.
- Rodriguez-Carbonell. E.. Kapur. D.. 2007-04-01. Generating all polynomial invariants in simple loops. Journal of Symbolic Computation. en. 42. 4. 443–476. 10.1016/j.jsc.2007.01.002. 0747-7171. free.
- Kapur. D.. 2006. Baader. Franz. Baumgartner. Peter. Nieuwenhuis. Robert. Voronkov. Andrei. Automatically Generating Loop Invariants Using Quantifier Elimination. Deduction and Applications. Dagstuhl Seminar Proceedings. Dagstuhl, Germany. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany.
- Book: Kapur . D.. Programming Logics . Elimination Techniques for Program Analysis . Lecture Notes in Computer Science. 2013 . 7797 . 194–215 . 10.1007/978-3-642-37651-1_8. 978-3-642-37650-4.
- Book: Kapur . D.. Majumdar . R.. Zarba . C.G. . Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering . Interpolation for data structures . 2006 . 105–116 . 10.1145/1181775.1181789. 1595934685. 158878.
- Ghilardi . S. . Gianola . A. . Kapur . D. . Computing Uniform Interpolants for EUF via (conditional) DAG-based Compact Representations . Italian Conference on Computational Logic . 67–81 . 2020 .
- Kapur. D.. Narendran. P.. 1992-10-01. Complexity of unification problems with associative-commutative operators. Journal of Automated Reasoning. en. 9. 2. 261–288. 10.1007/BF00245463. 26828762. 1573-0670.
- Benanav. D.. Kapur. D.. Narendran. P.. 1987-02-04. Complexity of matching problems. Journal of Symbolic Computation. en. 3. 1–2. 203–216. 10.1016/S0747-7171(87)80027-5. 0747-7171.
- Kapur . D.. Musser . D.. Narendran . P.. Stillman . J.. Semi-unification. Journal of Theoretical Computer Science . 1991 . 81. 2. 169–187. 10.1016/0304-3975(91)90189-9. 10.1.1.90.1272.
Notes and References
- Towards a Theory for Abstract Data Types. Deepak Kapur Ph.D. thesis. . June 1980 . https://web.archive.org/web/20210928212156/https://apps.dtic.mil/sti/citations/ADA085877 . live . September 28, 2021 . 28 September 2021. Kapur . Deepak .
- Web site: Faculty Profiles: Deepak Kapur. CS UNM . 28 September 2021.
- News: 5 August 2009 . Herbrand Award: for Distinguished Contributions to Automated Reasoning . Conference on Automated Deduction . 2021-09-28.
- Web site: Deepak Kapur Publications . 2021-09-28.
- Book: Kapur . Deepak . Sivakumar . G. . Zhang . Hantao . 8th International Conference on Automated Deduction . RRL: A rewrite rule laboratory . Lecture Notes in Computer Science . 1986 . 230 . 691–692 . 10.1007/3-540-16780-3_140. 978-3-540-16780-8 .
- Web site: The Tecton Project . 28 September 2021.