Deepak Kapur

Deepak Kapur
Born	August 24, 1950 Amritsar, Punjab, India
🏳️ Nationality	Indian, American
🎓 Alma mater	Indian Institute of Technology Kanpur Massachusetts Institute of Technology
💼 Occupation
👩 Spouse(s)	Roli Varma
👶 Children	Ila Kapur Varma
🏅 Awards	Herbrand Award (2009)
🌐 Website	https://www.cs.unm.edu/~kapur/

Deepak Kapur (born August 24, 1950) is a Distinguished Professor in the Department of Computer Science at the University of New Mexico

Bibliography

Born to a lower-middle-class family based in Amritsar, where his father, Nawal Kishore Kapur, was a cloth merchant and broker; and mother, Bimlavati Kapur, a housewife.

Kapur received the Herbrand Award in 2009:

in recognition of his seminal contributions to several areas of automated deduction including inductive theorem proving, geometry theorem proving, term rewriting, unification theory, integration and combination of decision procedures, lemma and loop invariant generation, as well as his work in computer algebra, which helped to bridge the gap between the two areas.

Education

Government Primary School, Katra Khazana, Amritsar, until 3rd grade, Vidya Bhushan School, Amritsar, until 5th grade, DAV High School until 11th grade, and IIT, Kanpur, 1966-73, B Tech graduated in May 1971, M. Tech graduates in May 1973.

Research

Kapur has published over 150 papers on Automated Theorem Proving, Term Rewriting, Inductive Theorem Proving, Unification Theory, and Complexity of Automated Reasoning Algorithms, Congruence Closure, Geometry Theorem Proving, Groebner basis, Comprehensive Groebner Basis, Multivariate Dixon Resultants, Software and Hardware Verification, Automated Derivation of Loop Invariants and Interpolation .

Kapur developed the Rewrite Rule Laboratory (RRL), the world’s first theorem prover based on term rewriting and the Knuth-Bendix completion procedure and its generalization . The theorem prover mechanized equational, first-order, and inductive reasoning. At General Electric Corporate Research and Development Center, Kapur designed and led the development of GeoMeter, a system for geometric and algebraic reasoning based on Groebner basis and comprehensive Groebner basis for applications to geometry theorem proving and computer vision. At the University at Albany, State University of New York, Kapur led the development of Tecton for hierarchical proof management . This system was built on top of RRL. These systems have been used in applications of hardware verification, specification analysis, geometric modeling, and computer vision.

Selected Publications

• Donald, B.R.; Kapur, D.; Mundy, J.L. (1992). Symbolic and Numerical Computation for Artificial Intelligence. Academic Press. ISBN 978-0-12-220535-4. Search this book on

• Kapur, D.; Mundy, J.L. Geometric Reasoning | The MIT Press. mitpress.mit.edu. MIT Press. Retrieved 2021-06-06. Search this book on

• Kapur, D.; Zhang, H. (1995-01-01). "An overview of 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, D.R. (October 1994). "An overview of the Tecton proof system". Theoretical Computer Science. 133 (2): 307–339. doi:10.1016/0304-3975(94)90192-9.

• Zhang, H.; Kapur, D.; Krishnamoorthy, M.S. (1988-05-23). "A mechanizable induction principle for equational specifications". 9th International Conference on Automated Deduction. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg. 310: 162–181. doi:10.1007/BFb0012831. ISBN 3-540-19343-X.

• Kapur, D.; Narendran, P. (1985-01-01). "A finite thue system with decidable word problem and without equivalent finite canonical system". Theoretical Computer Science. 35: 337–344. doi:10.1016/0304-3975(85)90023-4. ISSN 0304-3975.

• Benanav, D.; Kapur, D.; Narendran, P. (1987-02-04). "Complexity of matching problems". Journal of Symbolic Computation. 3 (1–2): 203–216. doi:10.1016/S0747-7171(87)80027-5. ISSN 0747-7171.

• Kapur, D.; Musser, D.R. (1987-02-01). "Proof by consistency". Artificial Intelligence. 31 (2): 125–157. doi:10.1016/0004-3702(87)90017-8. ISSN 0004-3702.

• Kapur, D.; Giesl, J.; Subramaniam, M. (2004). "Induction and Decision Procedures". Rev.R. Acad. Cien. Serie A. Mat. CiteSeerX 10.1.1.70.2434.

• Kapur, D.; Narendran, P. (1992-10-01). "Complexity of unification problems with associative-commutative operators". Journal of Automated Reasoning. 9 (2): 261–288. doi:10.1007/BF00245463. ISSN 1573-0670.

• Kapur, D.; Narendran, P. (1985-08-01). "An equational approach to theorem proving in first-order predicate calculus". ACM SIGSOFT Software Engineering Notes. 10 (4): 63–66. doi:10.1145/1012497.1012521. ISSN 0163-5948.

• Kapur, D.; Musser, D.; Narendran, P.; Stillman, J. (1991). "Semi-unification". Journal of Theoretical Computer Science. 81 (2): 169–187. CiteSeerX 10.1.1.90.1272. doi:10.1016/0304-3975(91)90189-9.

• Kandri-Rody, A.; Kapur, D.; Winkler, F. (1989). "Knuth-Bendix procedure and Buchberger algorithm: a synthesis". Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation - ISSAC '89: 55–67. doi:10.1145/74540.74548. ISBN 0897913256.

• Kandri-Rody, Ä.; Kapur, D. (1 August 1988). "Computing a Grobner basis of a polynomial ideal over a Euclidean domain". Journal of Symbolic Computation. 6 (1): 37–57. doi:10.1016/S0747-7171(88)80020-8. ISSN 0747-7171.

• Kapur, D. (1986-12-01). "Using Gröbner bases to reason about geometry problems". 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). "Wu's method and its application to perspective viewing". Artificial Intelligence. 37 (1–3): 15–36. doi:10.1016/0004-3702(88)90048-3. ISSN 0004-3702.

• Michel, J.D.; Nandhakumar, N.; Saxena, T.; Kapur, D. (1 October 1998). "Geometric, Algebraic, and Thermophysical Techniques for Object Recognition in IR Imagery". Computer Vision and Image Understanding. 72 (1): 84–97. doi:10.1006/cviu.1997.0669. ISSN 1077-3142.

• 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. doi:10.1137/S0036142995281504. ISSN 0036-1429.

• Kapur, D.; Madlener, K. (1989). "A Completion Procedure for Computing a Canonical Basis for a k-Subalgebra". Computers and Mathematics: 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). "Algebraic and geometric reasoning using Dixon resultants". Proceedings of the International Symposium on Symbolic and Algebraic Computation. ISSAC '94. Oxford, United Kingdom: Association for Computing Machinery: 99–107. doi:10.1145/190347.190372. ISBN 978-0-89791-638-7.

• Chtcherba, A.; Kapur, D. (1 July 2004). "Constructing Sylvester-type resultant matrices using the Dixon formulation". Journal of Symbolic Computation. 38 (1): 777–814. doi:10.1016/j.jsc.2003.11.003. ISSN 0747-7171.

• Chtcherba, A.D.; Kapur, D. (September 2003). "Exact resultants for corner-cut unmixed multivariate polynomial systems using the Dixon formulation". Journal of Symbolic Computation. 36 (3–4): 289–315. doi:10.1016/S0747-7171(03)00084-1.

• Kapur, D.; Subramaniam, M. (September 2000). "Using an induction prover for verifying arithmetic circuits". International Journal on Software Tools for Technology Transfer. 3 (1): 32–65. doi:10.1007/PL00010808.

• Falke, S.; Kapur, D. (2015). "When Is a Formula a Loop Invariant?". Logic, Rewriting, and Concurrency. Lecture Notes in Computer Science. 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). "Generating all polynomial invariants in simple loops". 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, eds. "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.

• Kapur, D. (2013). "Elimination Techniques for Program Analysis". Programming Logics. Lecture Notes in Computer Science. 7797: 194–215. doi:10.1007/978-3-642-37651-1_8. ISBN 978-3-642-37650-4.

• Kapur, D. (1993). "An Approach for Solving Systems of Parametric Polynomial Equations in". Principles and Practices of Constraint Programming. CiteSeerX 10.1.1.39.9091. Search this book on

• Kapur, D. (February 2017). "Comprehensive Gröbner basis theory for a parametric polynomial ideal and the associated completion algorithm". Journal of Systems Science and Complexity. 30 (1): 196–233. doi:10.1007/s11424-017-6337-8.

• Kapur, D.; Majumdar, R.; Zarba, C.G. (2006). "Interpolation for data structures". 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.

• Ghilardi, S.; Gianola, A.; Kapur, D. (2020). "Computing Uniform Interpolants for EUF via (conditional) DAG-based Compact Representations". Italian Conference on Computational Logic: 67–81.

• Varma, R.; Kapur, D. (23 April 2015). "Decoding femininity in computer science in India". Communications of the ACM. 58 (5): 56–62. doi:10.1145/2663339.

• Varma, R.; Kapur, D. (August 2013). "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. 15 (4): 315–330. doi:10.1080/13876988.2013.810376.

Academic Career

• GE Corporate R&D, 1980-1987
• SUNY Albany, 1988-1998, hired as a tenured full professor. In 1998, Kapur got distinguished research award.

• Kapur becomes Chair of the Computer Science department at the University of New Mexico, from 1998 until 2006. In 2007, Kapur becomes Distinguished Professor. In May, 2010, Kapur was awarded Senior Faculty Research Excellence Award by the School of Engineering of the University of New Mexico.

• Visiting appointments include Massachusetts Institute of Technology, Max Planck Institute for Informatics, IMDEA, Tata Institute of Fundamental Research, Indian Institute of Technology, Delhi, Institute of Software, the Chinese Academy of Sciences.

• Consultant to GE Corporate Research and Development, Sandia National Labs, Fujitsu Labs, IBM Research at Watson.

• Editor-in-Chief of Journal of Automated Reasoning, 1993-2007, and a member of the editorial boards of Journal of Automated Reasoning, Journal of Symbolic Computation, Leibniz International Proceedings in Informatics.

• Kapur was a Board Member of United Nation University - Computing and Society, United Nations University - Internal Institute for Software Technology, Computer Science Research Institute - Sandia National Laboratories, Los Alamos Computer Science Institute, International Federation of Computational Logic.

References

This article "Deepak Kapur" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:Deepak Kapur. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.

This page exists already on Wikipedia.

📰 Article(s) of the same category(ies)

• NTS-KEM
• Belgrade Assembly (1–2 January 1810)
• Rohit Srivastava
• The Falcon 147
• Feedzai
• The Epistles
• Gail Cramer

---