Comment «Isabelle» (le prouveur de théorèmes) a-t-elle obtenu son nom?

11

Le titre dit tout, mais je suis curieux car il n'est pas évident de savoir comment un prouveur de théorème a été nommé «Isabelle». Était-il nommé d'après une personne? Je n'ai pas pu le découvrir par certaines recherches Google.

history automated-theorem-proving isabelle IIM
la source
2
Avez-vous essayé de demander sur une liste de diffusion d'utilisateurs Isabelle?
DW
Je n'ai pas - je n'ai jamais utilisé Isabelle moi-même - je n'ai lu qu'un article qui l'utilisait.
IIM
1
Cette question me semble être hors sujet car il s'agit de l'histoire d'un artefact logiciel, pas d'un artefact CS. Cela dit, des articles ont été publiés sur Isabelle donc je vais laisser la communauté décider.
Raphael
Wikipédia mis à jour :-)
Mark Hurd

Réponses:

9

Un petit google-fu (et ma propre mémoire) me dit qu'il a apparemment été nommé par Larry Paulson d'après la fille de Gerard Huet .

Gerard Huet se trouve être l'une des personnes derrière le prouveur de théorème de Coq moins poétiquement nommé .

Petit monde!

cody
la source
1
Comment le nom Coq est-il moins poétique? C'est un jeu de mots sur pas moins de trois mots (le Calcul des Constructions CoC, l'un des fondateurs de la théorie Thierry Coquand, et le mot français pour coq (qui est un emblème de la France, et la plupart des fondateurs du Coq étaient français)) .
Gilles 'SO- arrête d'être méchant'
Le nom Coq est certainement intelligent (il y avait une contrainte supplémentaire que les langues de programmation académiques ont été nommées d' après un animal, voir par exemple Ocaml) mais je ne pense que c'est un peu moins poétique, en particulier compte tenu du jeu de mots supplémentaires (en anglais au moins) que je ne serais 't mis au-delà de Gerhard Huet pour être intentionnel.
cody