# Natarajan Shankar

Natarajan Shankar est un informaticien indien travaillant au SRI International à Menlo Park, en Californie, où il dirige le laboratoire d'analyse symbolique.

## Formation

Shankar obtient son doctorat. diplôme en informatique, sous la direction de Robert S. Boyer et J Strother Moore, de l'université du Texas à Austin en 1986.
Sa thèse de doctorat est publiée sous le titre de livre "Metamathematics, Machines, and Goedel's Proof" par Cambridge University Press en 1994.

## Carrière

Shankar est d'abord associé de recherche à l'université Stanford, de 1986 à 1988. En 1989, il rejoint le Laboratoire d'Informatique de SRI International. Au SRI, il utilise le prouveur de théorèmes de Boyer-Moore (en) pour prouver des métathéorèmes tels que le théorème de tautologie, le théorème d'incomplétude de Godel et la propriété de Church-Rosser. Il contribue au développement de la technologie de raisonnement automatisé, des systèmes déductifs et des moteurs de calcul, y compris le système de vérification de prototype.
Prix et distinctions En 2009, il est nommé SRI Fellow, aux côtés de Peter G. Neumann (en), John Rushby (en), Patrick Lincoln (en) et Carolyn Talcott (en). La bourse reconnaît les membres exceptionnels du personnel pour leurs contributions exceptionnelles à la science. En 2022 il est lauréat du prix Herbrand « en reconnaissance de ses travaux très influents dans plusieurs domaines du raisonnement automatique, notamment dans la formalisation des preuves, la coopération de procédures interactives de démonstration de théorèmes et de décision, et les applications à la vérification ».

## Publications

* (en) Patrick Lincoln, John Mitchell, Andre Scedrov et Natarajan Shankar, « Decision problems for propositional linear logic », Annals of Pure and Applied Logic, Elsevier, vol. 56, n$^{os}$ 1-3,‎ avril 1992, p. 239-311 (ISSN 0168-0072 et 1873-2461, DOI 10.1016/0168-0072(92)90075-B).
* (en) Natarajan Shankar et Marc Vaucher, « The Mechanical Verification of a DPLL-Based Satisfiability Solver », Electronic Notes in Theoretical Computer Science, Elsevier, vol. 269,‎ 19 avril 2011, p. 3-17 (ISSN 1571-0661, DOI 10.1016/J.ENTCS.2011.03.002).
* (fr + en) Natarajan Shankar, « Larry Wos, Ross Overbeek, Ewing Lusk, and Jim Boyle. Automated reasoning. Introduction and applications. Second edition of LI 464. McGraw-Hill, New York etc. 1992, xvi + 656 pp. + disk. », Journal of Symbolic Logic, Association for Symbolic Logic, vol. 59, n$^o$ 4,‎ décembre 1994, p. 1437-1439 (ISSN 0022-4812 et 1943-5886, OCLC 01782331, DOI 10.2307/2275719).
* (en) Maria Paola Bonacina, Stéphane Graham-Lengrand et Natarajan Shankar, « Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs », Journal of Automated Reasoning, Springer Science+Business Media, vol. 66, n$^o$ 1,‎ 12 septembre 2021, p. 43-91 (ISSN 0168-7433 et 1573-0670, OCLC 263592661, DOI 10.1007/S10817-021-09606-Y).
* (en) Natarajan Shankar, Natarajan Saravanakumar, Chandrasekaran Kumar, Vijayarangan Kamatchi Kannan et Balasubramanian Indu Rani, « Opposition-based equilibrium optimizer algorithm for identification of equivalent circuit parameters of various photovoltaic models », Journal of Computational Electronics, Springer Science+Business Media, vol. 20, n$^o$ 4,‎ 31 mai 2021, p. 1560-1587 (ISSN 1569-8025 et 1572-8137, DOI 10.1007/S10825-021-01722-7).