ASSISTANT DE PREUVE, informatique

Ce sujet est traité dans les articles suivants :

1.  INFORMATIQUE ET VÉRITÉ MATHÉMATIQUE

Écrit par : Jean-Paul DELAHAYE

Dans le chapitre "Preuves mathématiques classiques avec ordinateur"  : … 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 de preuve ». L'écriture complète d'une démonstration formelle, comme Hilbert le demandait,… Lire la suite

2.  MILNER ROBIN (1934-2010)

Écrit par :  Universalis

…  aux côtés de John McCarthy au laboratoire d'intelligence artificielle de l'université Stanford. *Il y développe le système L.C.F. (Logic for Computable Functions), l'un des premiers logiciels de preuve de programmes fondés sur des principes mathématiques rigoureux. De retour au Royaume-Uni en 1973, il intègre l'université d'Édimbourg, où il… Lire la suite

3.  PROGRAMMATION

Écrit par : Jean-François MONIN

Dans le chapitre "Quelques approches formelles"  : … logique temporelle. À 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 architecturés autour d'un… Lire la suite