Types de fournisseurs de théorèmes automatisés

20

J'apprends moi-même la vérification automatisée de théorèmes / les solveurs SMT / assistants de vérification et je poste une série de questions sur le processus, en commençant ici .

Quels sont les prouveurs de théorèmes automatisés pertinents? J'ai trouvé un examen des théoriciens

Est-ce toujours d'actualité?

Lesquels sont encore très actifs, c'est-à-dire ceux qui sont actuellement utilisés au-delà du groupe qui les a créés?

Trouvez la prochaine question de la série ici .

Guy Coder
la source

Réponses:

15

La catégorisation dans cette liste est certainement toujours d'actualité.

Peut-être qu'une nouvelle catégorie a émergé, à savoir les langages de programmation de type dépendant . Ce sont essentiellement des prouveurs de théorèmes automatisés dont le but principal n'est pas de prouver des théorèmes, mais de programmer. En raison de la correspondance Curry-Howard , ces deux concepts sont étroitement liés. Le but ultime de ces langages de programmation est d'écrire des programmes qui ont des garanties beaucoup plus fortes que les langages de programmation typés classiques. Les gens les utilisent également pour prouver le théorème. Certains nouveaux systèmes entrant dans cette catégorie incluent Agda et Epigram. L'une des principales caractéristiques de ces langages est qu'ils mettent beaucoup d'efforts pour faciliter la définition par les programmeurs de familles inductives de types de données. Un exemple simple est un vecteur, qui dépend de nombres naturels (définis par induction).

En ce qui concerne ceux qui sont encore très actifs, je pense qu'ils le sont tous. Coq , Isabelle , Twelf et PVS sont beaucoup utilisés dans la communauté des langages de programmation. Maude est largement utilisé dans les systèmes de modélisation. (Personnellement, j'ai utilisé Coq et Maude .)

Je n'en avais jamais entendu parler. Dans le pdf vers lequel vous créez un lien, il existe des liens vers les prouveurs de théorèmes. Certains liens sont actuels, d'autres sont rompus. Gandalf semble maintenant être une sorte de sorcier barbu.

Les prouveurs de théorèmes mentionnés dans «A Review of Theorem Provers» sont:

  • ALF : subsumbed par ALFA, Coq et Agda.
  • ALFA : semble ne plus être pris en charge.
  • COQ : activement soutenu.
  • MetaPRL : semble ne plus être pris en charge.
  • NuPRL : activement pris en charge.
  • HOL : activement soutenu.
  • PVS : activement soutenu.
  • Isabelle : activement soutenue.
  • DOUZE : activement soutenu.
  • ACL2 : activement pris en charge.
  • INKA : semble ne plus être pris en charge.
  • GANDALF : semble ne plus être pris en charge.
  • TPS : peut encore être actif, mais n'a qu'un petit nombre d'abonnés.
  • OTTER : peut ne plus être pris en charge.
  • SETHEO : remplacé par E-SETHEO, qui ne semble plus être pris en charge.
  • SPASS : semble être encore actif.
  • EQP : semble ne plus être pris en charge.
  • MAUDE : très activement soutenu.
  • OMEGA : ne semble plus être pris en charge.
  • Mizar : activement soutenu.

Il existe sans aucun doute de nombreux nouveaux prouveurs de théorèmes automatisés qui n'ont pas été mentionnés dans cette liste.

Par souci d'exhaustivité, comme l'a suggéré Raphaël , il existe des preuves d'archivage de sites réalisées à l'aide de divers outils. Par exemple:

Dave Clarke
la source
2
Il est probablement utile de créer un lien vers des (listes de) preuves où les outils respectifs ont été utilisés, par exemple Archive of Proofs pour Isabelle.
Raphael
@GuyCoder: Pour une raison quelconque, vos ajouts ont été supprimés. Je les ai rajoutés.
Dave Clarke
«Certains nouveaux systèmes entrant dans cette catégorie incluent Agda et Epigram.»: Semble avoir disparu. Y a-t-il un nouvel emplacement pour Eprigram? Ou une alternative proche?
Hibou57
1
«En ce qui concerne ceux qui sont encore très actifs, je pense qu'ils le sont tous. Coq, Isabelle, Twelf et PVS »: PVS est connu pour avoir des bugs de solidité. Contrairement à Isabelle et Coq, PVS ne suit pas l'architecture micro-noyau. Recherchez le critère De Bruijn pour savoir pourquoi il est important.
Hibou57
1
Outre Agda et (défunt?) Epigram, il y a le langage de programmation ATS , qui selon sa liste de diffusion, semble être actif jusqu'à présent en 2014.
Hibou57