Aprendendo a comprovação do teorema automatizado

44

Estou aprendendo sozinho os provedores de teoremas automatizados / solucionadores de SMT / assistentes de prova e postar uma série de perguntas sobre o processo, começando aqui.

Observe que esses tópicos não são facilmente digeridos sem um histórico em lógicas (matemáticas). Se você tiver problemas com termos básicos, leia-os, por exemplo, Lógica em Ciência da Computação, por M. Huth e M. Ryan (em particular, capítulos um, dois e quatro) ou Uma Introdução à Lógica Matemática e Teoria dos Tipos, por P. Andrews.
Para uma breve introdução à lógica de ordem superior (HOL), clique aqui .

Olhei para Coq e li o primeiro capítulo da introdução para Isabelle, entre outros; Tipos de provedores de teoremas automatizados

Conheço o Prolog há algumas décadas e agora estou aprendendo F #, então ML, O'Caml e LISP são um bônus. Haskell é um animal diferente.

Eu tenho os seguintes livros

"Manual de raciocínio automatizado", editado por Alan Robinson e Andrei Vornkov

"Manual de lógica prática e raciocínio automatizado", de John Harrison

"Reescrita de Termos e Tudo Isso", de Franz Baader e Tobias Nipkow

  1. Quais são as diferenças entre Coq e Isabelle?

  2. Devo aprender Isabelle ou Coq, ou ambos?

  3. Existe uma vantagem em aprender Isabelle ou Coq primeiro?

Encontre a próxima pergunta da série aqui .

Guy Coder
fonte
7
É importante observar que as ferramentas mencionadas não são provadores automatizados, mas assistentes de prova (embora possam provar coisas fáceis por conta própria).
Raphael
@DaveClarke Duplicate?
Raphael
@ Rafael: Sim (exceto agora a minha resposta contém novos dados).
Dave Clarke
@DaveClarke Você acha que devemos fechar este e fundir os dois?
Raphael
@ Rafael: Sim. Acabei de copiar o texto da resposta aqui para minha outra pergunta.
Dave Clarke

Respostas:

25

Minha preferência é por Coq, mas imagino que outros prefiram Isabelle. Uma das coisas estranhas que descobri sobre Isabelle é que há uma sintaxe de dois níveis, onde algumas de suas definições precisam estar entre aspas duplas. Esse absurdo não está presente na Coq.

Por fim, o que é mais adequado para você pode depender do que você deseja provar. Os dois idiomas têm muito suporte a bibliotecas e comunidades ativas, desenvolvendo todo tipo de teoria de desenvolvimento e exemplo. Se um idioma fornece suporte adequado à biblioteca (ou outro) para os tipos de teoria que você deseja desenvolver, selecionaria esse idioma.

Uma estratégia é fazer um tutorial simples nos dois idiomas e acompanhar o que se sente melhor. Por exemplo,

Aqui está uma postagem no blog comparando os dois por alguém que prefere Isabelle.

Certifique-se de usar um IDE adequado (como ProofGeneral ), em vez de fazer as coisas na linha de comando.

Outra maneira de entrar na Coq é experimentar o livro online Software Foundations, de Benjamin Pierce et al. Ele fornece um excelente tutorial com muitos detalhes fornecidos. O foco está principalmente na semântica da linguagem de programação, mas muitas das bases (e além) da prova de Coq e do teorema semi-automatizado são abordadas ao longo do caminho.

Dave Clarke
fonte
4
O ProofGeneral é incrível, depois de domar! Com relação à sintaxe de Isabelle: iirc, coisas entre aspas duplas são as coisas sobre as quais você fala, as fórmulas. Tudo o resto é controle de prova. Eu pensei que a distinção clara era boa, mas aspas duplas (e a consequente falta de destaque de sintaxe dentro das aspas) provavelmente não é a melhor maneira de implementá-la.
Raphael
4
Criamos um wiki de Isabelle / HOL no ano passado para um curso; tem algumas visões gerais difíceis de encontrar, caso contrário.
Raphael
18

Uma coisa que eu acho que você achará interessante é que o termo "prova de teoremas" varia muito, dependendo do campo em que você está. Enquanto eles são - em resumo - um pouco relacionados à prova prática de teoremas práticos (como o tipo que você ver elaborado no Manual de raciocínio automatizado) tem menos a ver com Coq ou Isabelle do que você imagina.

Quando me propus a aprender sobre o teorema de provar coisas relacionadas, o primeiro livro que li (embora já esteja datado?) Foi a excelente lógica de primeira ordem de Melvin Fitting e a prova automatizada de teoremas. Este livro foi realmente excelente e abordou os tipos de tópicos que você verá relacionados às lógicas de ordem inferior, onde você pode obter uma quantidade razoável de automação. O tipo de lógica que você aprende deve ser ditado pelo que você quer raciocinar, e não tanto pelo teorema que prove isso. Por exemplo, enquanto a lógica de primeira ordem oferece uma quantidade razoável de expressividade e capacidade de raciocínio, a maioria da comunidade de linguagens de programação (onde acabei hoje em dia) partiu da escola mais antiga de prova de teoremas e verificação de modelos (que entra em cena o balde de coisas que são mais decidíveis, mas menos expressivas).

No entanto, não entenda que coisas como raciocínio de primeira ordem e verificação de modelos não foram extremamente úteis na prática. Eles têm sido! Você pode ver o ACL2 como um exemplo de um testador construído sobre a lógica de primeira ordem que obteve uma incrível quantidade de sucesso no setor industrial. Junto com isso, também houve uma quantidade incrível de desenvolvimento na solução SMT. Os solucionadores SMT modernos são criados com base em solucionadores SAT muito poderosos (principalmente através de descobertas nos últimos vinte anos para melhorias no DPLL) e têm visto uma grande quantidade de uso em coisas como execução simbólica.

No entanto, como eu disse, embora a parte mais tradicional de "prova de teoremas" seja divertida, há muito mais a aprender. Aprender Coq - por exemplo - tem pouco a ver com o aprendizado das ferramentas de automação que ele fornece, e tem muito mais a ver com o aprendizado da teoria dos tipos em que se baseia (o cálculo predicativo de construções coindutivas). Se você não está acostumado à lógica construtiva, ao isomorfismo de curry howard ou à teoria dos tipos, passará um tempo emocionante aprendendo essas ferramentas, mas mal posso pensar que elas estejam intimamente relacionadas às coisas que você vê no primeiro volume. do manual.

Portanto, decida o que você quer fazer: verifique modelos e teoremas na lógica de primeira ordem ou use uma poderosa teoria de tipos para raciocinar sobre a correção de seus programas (ou teoremas na lógica construtiva). Se for o primeiro, aprenda sobre técnicas baseadas em dedução mais automatizadas, se for o segundo, aprenda mais sobre Coq, HOL, etc ... A propósito, se você quiser aprender Coq, enquanto as referências acima são boas, acho que existem duas referências realmente essenciais para aprender Coq:

Livro de fundações de software de Benjamin Pierce (Dr. Pierce é um excelente escritor, e eu recomendo que você também olhe para o mais popular "livro de tijolos", se ainda não o fez).

Programação certificada com tipos dependentes (Adam Chlipala também escreve muito bem, embora seus livros tenham um pouco mais de maturidade e inteligência do que a introdução talvez mais simples de Pierce).

Kristopher Micinski
fonte
15

Existe uma variedade de sistemas para Provas de Teoremas Interativos (ITP) - veja também a conferência com esse nome - Coq, Isabelle, HOLs, ACL2, PVS etc.

Todos eles são relativamente difíceis de aprender, e cada um tem sua própria cultura específica. É como aprender uma língua estrangeira: digamos que você já saiba inglês e depois tenha a opção de francês, alemão, italiano, espanhol, português. Todos eles estão de alguma forma relacionados - isso não é chinês -, mas poucas pessoas gerenciam tudo isso simultaneamente. Portanto, você deve experimentar um gostinho de cada uma das culturas e comunidades e depois se comprometer.

Pode haver também o "recurso matador" que você realmente precisa para o seu trabalho.

Também ajuda a ter colegas especialistas em um desses sistemas.

  • Quais são as diferenças entre Coq e Isabelle?

Ambos são descendentes do sistema LCF de Stanford / Edinburgh / Cambridge. Em 1985, G. Huet e L. Paulson estavam trabalhando juntos na última versão do Cambridge LCF. Então a divisão aconteceu em direção a Coc / CIC / COQ (agora Coq) na França, e Isabelle em Cambridge e Munique. Observe que HOL4, HOL-Light, HOL-XYZ são outros descendentes relacionados ao LCF.

Há mais de 20 anos, a distinção entre Coq e Isabelle teria sido feita de acordo com fundamentos lógicos: lógica construtiva dependentemente digitada aqui, lógica clássica simplificada ali. Hoje, surpreendentemente, há pouco impacto nisso na prática, uma vez que mais e mais camadas foram adicionadas sobre cada sistema formal, incluindo ferramentas complementares e bibliotecas.

  • Devo aprender Isabelle ou Coq, ou ambos?

Você deve olhar para os dois e tentar sentir se gosta de mais vinho e queijo ou bratwurst e chucrute. (Como um dos caras por trás de Isabelle, mas atualmente na França, estou surpreso com quantos franceses realmente gostam de chucrute quando estão em casa e ninguém olhando :-)

  • Existe uma vantagem em aprender Isabelle ou Coq primeiro?

Acho que não. Pode haver o perigo de você ficar preso com o que você tenta primeiro e não tentar o segundo, ou se decepcionar muito cedo com o primeiro e descartá-lo muito cedo. De qualquer forma, você precisará de tempo e persistência para se tornar produtivo com qualquer um dos sistemas.

Como a Prova Geral como "IDE" já foi mencionada: A Prova Geral / Emacs costumava ser a interface unificadora padrão da Coq e da Isabelle ao longo de muitos anos, mas eu nunca a chamaria de IDE. Há também o CoqIDE com "IDE" em seu nome, mas é um editor relativamente básico sobre os widgets Gtk. Isabelle atual inclui Isabelle / jEdit, que não tem "IDE" em seu nome, mas pretende aproximar coisas que você vê rotineiramente no Netbeans ou no IntelliJ IDEA --- para textos de prova em vez de código Java.

Makarius
fonte
10

Aqui estão alguns tutoriais em Coq de Andrej Bauer. Não está completo, mas acho que é uma boa introdução.

Daniil
fonte
11
Ótimo! Observe uma frase central em "Uma primeira prova com Coq": "Pense em como você faria isso no papel". Melhor conselho de todos os tempos.
Raphael
4

Esta introdução a Isabelle é bastante exaustiva.

Veja também esta introdução a Isabelle

Em geral, Isabelle é relativamente fácil de começar, pois há muitos exemplos disponíveis. Por exemplo, no site oficial

PS - Eu não sou afiliado de nenhuma maneira a Isabelle, sou um teórico em métodos formais, mas sei que Isabelle surge frequentemente como um ponto de partida padrão.

Shaull
fonte
11
“Eu sei que Isabelle aparece frequentemente como um ponto de partida padrão.”: Prefiro dizer que o HOL geralmente é um ponto de partida padrão e, como assistente de prova, é o Coq, que geralmente vem como padrão. Pensando nisso, isso é engraçado… a lógica mais famosa (HOL mais famosa que CoC) e a assistente de prova mais famosa (Coq mais famosa que Isabelle), não combinam (Coq é baseada em CoC e Isabelle em HOL).
Hibou57
2

λ

Além disso, o Software Foundations da DeepSpec Summer School tem algumas palestras bem legais:

Algumas das palestras baseadas na série de fundações de software, que já foram mencionadas.

Aristu
fonte