ASSISTANT DE PREUVE, informatique

INFORMATIQUE ET VÉRITÉ MATHÉMATIQUE

  • Écrit par 
  • Jean-Paul DELAHAYE
  •  • 1 990 mots
  •  • 1 média

Dans le chapitre « Preuves mathématiques classiques avec ordinateur »  : […] Si l'ordinateur peut conduire à de quasi-certitudes en dehors de la méthode hilbertienne, il peut aussi produire des preuves mathématiques classiques. Plusieurs cas sont possibles, que nous allons présenter en insistant sur ce qui les distingue. Certaines techniques de démonstration automatique produisent des démonstrations qu'aucun humain n'avait découvertes sans aide informatique, mais qui, une […] Lire la suite☛ http://www.universalis.fr/encyclopedie/informatique-et-verite-mathematique/#i_41378

MILNER ROBIN (1934-2010)

  • Écrit par 
  • Universalis
  •  • 600 mots

Le Britannique Robin Milner a été l'un des pionniers de la science informatique. Il avait reçu en 1991 le prix Turing, l'une des plus prestigieuses récompenses en informatique, pour ses contributions majeures aux fondements de ce domaine. Né le 13 janvier 1934 à Yealmpton, dans le Devon et issu d'un milieu modeste, Arthur John Robin Gorell Milner étudie à l'Eton College, puis obtient une bourse po […] Lire la suite☛ http://www.universalis.fr/encyclopedie/robin-milner/#i_41378

PROGRAMMATION

  • Écrit par 
  • Jean-François MONIN
  •  • 7 832 mots

Dans le chapitre « Quelques approches formelles »  : […] Deux obstacles techniques s'opposent au passage à l'échelle d'applications réelles. Il faut d'une part gérer des spécifications formelles de grandes dimensions et d'autre part faciliter le processus de démonstration. Cela a donné lieu à deux directions de recherche à partir des années 1970. L'une, illustrée par le langage Z, a développé un formalisme expressif fondé sur les notations ensemblistes. […] Lire la suite☛ http://www.universalis.fr/encyclopedie/programmation/#i_41378