¿Cómo obtuvo su nombre 'Isabelle' (el probador de teoremas)?

11

El título lo dice todo, pero tengo curiosidad porque no es obvio cómo un probador de teoremas llegó a llamarse 'Isabelle'. ¿Fue nombrado por una persona? No pude averiguar por algunas búsquedas de Google.

history automated-theorem-proving isabelle IIM
fuente
2
¿Has intentado preguntar en una lista de correo de usuarios de Isabelle?
DW
No lo he hecho, nunca he usado a Isabelle, solo he leído un periódico que lo usó.
IIM
1
Esta pregunta me parece fuera de tema, ya que se trata de la historia de un artefacto de software, no de un artefacto de CS. Dicho esto, se han publicado artículos sobre Isabelle, así que dejaré que la comunidad decida.
Raphael
Wikipedia actualizada :-)
Mark Hurd

Respuestas:

9

Un pequeño google-fu (y mi propia memoria) me dice que aparentemente fue nombrado por Larry Paulson en honor a la hija de Gerard Huet .

Gerard Huet es una de las personas detrás del probador de teoremas de Coq menos poéticamente llamado .

¡Mundo pequeño!

cody
fuente
1
¿Cómo es el nombre Coq menos poético? Es un juego de palabras con no menos de tres palabras (el Cálculo de construcciones CoC, uno de los fundadores de la teoría Thierry Coquand, y la palabra francesa para gallo (que es un emblema de Francia, y la mayoría de los fundadores de Coq eran franceses)) .
Gilles 'SO- deja de ser malvado'
El nombre Coq es sin duda inteligente (había una restricción adicional que los lenguajes de programación académicos fueron nombrados después de un animal, véase, por ejemplo Ocaml) pero yo no creo que sea un poco menos poética, especialmente teniendo en cuenta el juego de palabras adicionales (en Inglés por lo menos) que wouldn No pongas más allá de Gerhard Huet para que sea intencional.
cody