Foundations of Artificial Intelligence –
Automated Theorem Proving
(1988-1998)

Impact: Academic

Automated Theorem Proving, the cornerstone of “Strong AI”, refers to the ability to create intelligent machines that can implement the formal rules of deductive inference (modus ponens and modus tollens) and derive formal inferences from a set of axioms. In the mid-80s there was a program of research proposed by Professor Robert Jeroslow at Georgia Tech to improve the efficiencies of deductive logic using geometric methods. Jeroslow tragically, passed away soon after and Chandru & Hooker (Prof J N Hooker, Carnegie Mellon University) picked up the baton and through a ten year collaboration were major contributors in building out this research program. In addition to a series of research papers, this work resulted in “Optimization Methods for Logical Inference” a book in computational logic published by Wiley Interscience in 1999. During this period, Chandru was also a visiting academic with the Programming Languages Group at the IBM Watson Research Center at Hawthorne and Yorktown Heights.

·        V.Chandru and J.N.Hooker, An Extended Class of Horn Clause Systems, Journal of the Association for Computing Machinery, Vol 38, No. 1, January 1991, pp.  205-221.

·        V.Chandru, C.R.Coullard, P.L.Hammer, M.A.Montanez and X.Sun, On Renamable Horn and Generalized Horn Functions, Annals of Mathematics and Artificial Intelligence, Vol I, pp. 33-47, 1990.

·        Vivek S. Borkar, Vijay Chandru, Sanjoy K. Mitter: Mathematical Programming Embeddings of Logic. J. Autom. Reasoning 29(1): 91-106 (2002)

·        John N. Hooker, G. Rago, V. Chandru, A. Shrivastava: Partial Instantiation Methods for Inference in First-Order Logic. J. Autom. Reasoning 28(5): 371-396 (2002)