Richard Waldinger - Richard Waldinger

Richard Waldinger
Nationalité américain
mère nourricière L'université de Carnegie Mellon
Carrière scientifique
Les institutions SRI International
Conseiller doctoral Herbert A. Simon

Richard Jay Waldinger est un chercheur en informatique à SRI International du Centre d' intelligence artificielle (où il travaille depuis 1969) dont les intérêts portent essentiellement sur l'application automatisée raisonnement déductif à des problèmes dans le génie logiciel et l' intelligence artificielle .

Première vie et éducation

Dans sa thèse ( Carnegie Mellon University , 1969), qui portait sur l'extraction de programmes informatiques à partir de preuves de théorèmes, il a constaté que l'application de la règle de résolution expliquait l'apparition d'une branche conditionnelle dans le programme extrait, tandis que l'utilisation du Le principe d'induction mathématique a provoqué l'introduction de la récursivité et d'autres constructions répétitives.

Carrière

Waldinger a commencé à SRI International, alors connu sous le nom de Stanford Research Institute, en 1969, et y est resté depuis. Il sert du café et des biscuits dans son bureau au SRI deux fois par semaine depuis 1970.

QA4

Waldinger a collaboré avec Cordell vert, Robert Yates, Jeff Rulifson et Jan Derksen sur QA4 , un PLANNER , comme le langage de l' intelligence artificielle orientée vers la planification automatique et théorème proving. QA4 a introduit la notion de contexte et aussi d'unification associative-commutative, ce qui rendait les axiomes associatifs et commutatifs des opérateurs non seulement inutiles mais aussi inexprimables. Ils ont appliqué le langage à la planification du robot SRI, Shakey . Avec Bernie Elspas et Karl Levitt, Waldinger a utilisé QA4 pour la vérification de programme (prouvant qu'un programme fait ce qu'il est censé faire), obtenant des vérifications automatiques pour l'algorithme d'unification et le programme FIND de Hoare .

Synthèse du programme

Alors que la thèse de Waldinger avait traité de la synthèse de programmes applicatifs, qui retournent un résultat mais ne produisent aucun effet secondaire, Waldinger s'est alors tourné vers la synthèse de programmes impératifs, qui font les deux. Pour résoudre le problème de la réalisation simultanée d'objectifs qui interfèrent les uns avec les autres, il a introduit la notion de régression d'objectifs, qui a été obtenue à partir de travaux antérieurs sur la vérification de programme par Floyd , King, Hoare et Dijkstra . Puisque les programmes impératifs sont analogues aux plans, l'approche était également applicable aux problèmes classiques de planification de l'IA.

En collaboration avec Zohar Manna , de l'Université de Stanford , Waldinger a développé la résolution non clausale, une forme de résolution qui n'exigeait pas la traduction de phrases logiques en une forme clausale restreinte. Non seulement la traduction était coûteuse, mais elle compliquait parfois pathologiquement la preuve du théorème résultant; ces problèmes ont été contournés par la nouvelle règle. Ils ont appliqué la règle sur papier pour produire une synthèse détaillée d'un algorithme d'unification. Dans un autre article, ils ont synthétisé un nouvel algorithme de racine carrée; ils ont constaté que la notion de recherche binaire apparaît spontanément par une seule application de la règle de résolution à la spécification de la racine carrée.

SNARK

Certaines des idées de démonstration du théorème de Manna et Waldinger ont été incorporées dans la conception du prouveur de théorème SNARK de Mark Stickel . Les chercheurs de la NASA , dirigés par Mike Lowry, ont utilisé SNARK dans la mise en œuvre de l'environnement de développement logiciel Amphion, qui a été utilisé pour construire des programmes d'analyse des données des missions de la NASA pour les astronomes planétaires. Un logiciel construit automatiquement par Amphion a été utilisé pour planifier la photographie de la mission Cassini-Huygens NASA; c'est peut-être l'application la plus pratique à ce jour d'un logiciel construit automatiquement par des méthodes déductives.

Le système SNARK a été incorporé par le Kestrel Institute dans leur environnement de développement logiciel Specware, qui a été utilisé par Waldinger pour la validation de l'axiomatisation de premier ordre de DAML , le langage de balisage d'agent DARPA , et de son successeur, OWL . SNARK a découvert des incohérences non seulement dans les axiomes pour DAML, mais aussi dans les axiomes pour le langage fondateur KIF , sur lequel l'axiomatisation DAML était basée. Récemment, Waldinger a travaillé sur l'application de méthodes déductives pour répondre à des questions en géographie, biologie et analyse de l'intelligence. En collaboration avec le Kestrel Institute, il utilise SNARK pour authentifier les protocoles de sécurité.

Adhésions et récompenses

En 1991, Waldinger a été élu membre de l' Association pour l'avancement de l'intelligence artificielle .

Vie privée

Dans sa vie personnelle, Waldinger est un étudiant de l'aïkido, du yoga et de la méditation. Membre d'un groupe d'écriture établi, il a publié du journalisme culinaire et de la fiction érotique. Il est marié et père de deux enfants et de trois petits-enfants.

Références

Lectures complémentaires

  • Gerd Große et Richard Waldinger. "Vers une théorie des actions simultanées" EWSP 1991: 78-87.
  • Zohar Manna et Richard Waldinger. "L'origine d'un paradigme de recherche binaire" Sci. Comput. Programme. 9 (1): 37 à 83 (1987)

Liens externes