ASSISTANT DE PREUVE, informatique

Articles

• INFORMATIQUE ET VÉRITÉ MATHÉMATIQUE

  • Écrit par Jean-Paul DELAHAYE
  • 1 988 mots
  ...conjecture de Kepler. En décembre 2004, un fait nouveau s'est cependant produit, qui crée une situation sans précédent dans l'histoire des mathématiques : une démonstration formelle complète a été produite par Georges Gonthier, des Laboratoires Microsoft de Cambridge, en utilisant un logiciel appelé « assistant...

• MILNER ROBIN (1934-2010)

  • Écrit par Encyclopædia Universalis
  • 601 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...

• PROGRAMMATION

  • Écrit par Jean-François MONIN
  • 7 691 mots
  À partir des années 1980, une voie synthétique s'est développée, en proposant des assistants à la preuve, comme LCF, HOL, Isabelle, Coq et PVS, fondés sur une logique d'ordre supérieure, très expressive, tout en accueillant des procédures de décision sophistiquées. À l'exception du dernier, ils sont...