Como 'Isabelle' (a prova do teorema) recebeu esse nome?

11

O título diz tudo, mas estou curioso porque não é óbvio como um provador de teoremas foi chamado de 'Isabelle'. Foi nomeado para uma pessoa? Não consegui descobrir em algumas pesquisas no Google.

history automated-theorem-proving isabelle IIM
fonte
2
Você já tentou perguntar em uma lista de discussão dos usuários de Isabelle?
DW
Eu nunca - nunca usei Isabelle - li apenas um artigo que o usou.
IIM
1
Essa pergunta me parece fora de tópico, pois é sobre a história de um artefato de software, não de CS. Dito isto, foram publicados artigos sobre Isabelle, então deixarei a comunidade decidir.
Raphael
Wikipedia atualizado :-)
Mark Hurd

Respostas:

9

Um pequeno google-fu (e minha própria memória) me diz que aparentemente foi nomeado por Larry Paulson em homenagem à filha de Gerard Huet .

Gerard Huet é, por acaso, uma das pessoas por trás do menos provado poeticamente provador do teorema de Coq .

Mundo pequeno!

cody
fonte
1
Como o nome Coq é menos poético? É um trocadilho com não menos que três palavras (o Calculus of Constructions CoC, um dos fundadores da teoria Thierry Coquand, e a palavra francesa para galo (que é um emblema da França e a maioria dos fundadores da Coq eram franceses)) .
Gilles 'SO- stop be evil'
O nome Coq é certamente inteligente (não havia uma restrição adicional de que as linguagens de programação acadêmicos foram nomeados após um animal, ver, por exemplo Ocaml), mas eu não acho que é um pouco menos poética, especialmente tendo em conta o trocadilho adicional (em Inglês, pelo menos) que eu não iria colocar além de Gerhard Huet para ser intencional.
Cody