Как «Изабель» (доказатель теорем) получила свое имя?

Название говорит само за себя, но мне любопытно, потому что не очевидно, как доказатель теорем получил название «Изабель». Это было названо в честь человека? Я не мог узнать по некоторым поискам Google.

history automated-theorem-proving isabelle ММВ
источник

Вы пробовали спрашивать в списке рассылки пользователей Isabelle?

Я не - я никогда не использовал Изабель сам - я только прочитал газету, которая использовала это.

IIM

Этот вопрос поражает меня тем, что он является оффтопом, поскольку он касается истории программного артефакта, а не артефакта CS. Тем не менее, были опубликованы статьи об Изабель, поэтому я позволю сообществу принять решение.

Рафаэль

Википедия обновлена :-)

Марк Херд

Ответы:

Небольшое гугл-фу (и моя собственная память) говорит мне, что Ларри Полсон назвал его в честь дочери Джерарда Хуэта .

Джерард Хуэт, оказывается, один из тех, кто стоит за менее поэтически названным доказателем теорем Кока .

Маленький мир!

Коди
источник

Как имя Coq менее поэтично? Это каламбур не менее, чем на три слова (CoC «Исчисление конструкций», один из основателей теории Тьерри Кокванд, и французское слово « петух» (который является эмблемой Франции, а большинство основателей Coq были французами)) ,

Жиль "ТАК - перестань быть злым"

Название Coq, конечно, умное (было дополнительное ограничение, что академические языки программирования были названы в честь животных, см., Например, Ocaml), но я действительно думаю, что это немного менее поэтично, особенно с учетом дополнительного каламбура (по крайней мере на английском), который я бы не стал за Герхарда Хуэта быть намеренным.

cody