W jaki sposób nazwa „Isabelle” (przysłowiowa twierdzenie) ma swoją nazwę?

Tytuł mówi wszystko, ale jestem ciekawy, ponieważ nie jest oczywiste, jak to się stało, że nazwano go „Isabelle”. Czy to imię pochodzi od osoby? Niektórych wyszukiwań w Google nie mogłem się dowiedzieć.

history automated-theorem-proving isabelle

— IIM
źródło

Czy próbowałeś zapytać na liście adresowej użytkowników Isabelle?

— DW

Nie zrobiłem - sam nigdy nie korzystałem z Isabelle - czytałem tylko gazetę, która z niej skorzystała.

— IIM

Pytanie to wydaje mi się nie na temat, ponieważ dotyczy historii artefaktu oprogramowania, a nie artefaktu CS. To powiedziawszy, opublikowano artykuły o Isabelle, więc pozwolę społeczności decydować.

— Raphael

Aktualizacja Wikipedii :-)

— Mark Hurd

Trochę google-fu (i moja pamięć) mówi mi, że najwyraźniej został nazwany przez Larry'ego Paulsona po córce Gerarda Hueta .

Gerard Huet jest jednym z ludzi stojących za mniej poetycko uznanym twierdzeniem Coqa .

Mały świat!

— cody
źródło

Jak nazwa Coq jest mniej poetycka? Jest to gra słów nie mniejsza niż trzy słowa (Calculus of Constructions CoC, jeden z założycieli teorii Thierry Coquand i francuskie słowo oznaczające koguta (który jest symbolem Francji, a większość założycieli Coq to Francuzi)) .

— Gilles 'SO - przestań być zły'

Nazwa Coq pewnością jest mądry (nie było dodatkowym ograniczeniem, że języki programowania akademickie zostały nazwane zwierzęcia, patrz np SML), ale nie sądzę, że jest to nieco mniej poetycki, zwłaszcza biorąc pod uwagę dodatkowy pun (w języku angielskim przynajmniej), że Wouldn postawiła poza Gerhardem Huetem na celowość.

— cody