Eu gostaria de escrever provas matemáticas usando algum assistente de prova. Tudo será escrito usando lógica de primeira ordem (com igualdade) e dedução natural. O pano de fundo é a teoria dos conjuntos (ZF). Por exemplo, como eu poderia escrever a seguinte prova?
Axiom:
Teorema:
Ou seja, o conjunto vazio é único.
É trivial para mim fazer isso usando papel e caneta, mas o que realmente preciso é de um software para me ajudar a verificar as provas de correção.
Obrigado.
Respostas:
Coq e Isabelle podem fazer isso.
[Coq] Aqui está um artigo discutindo como codificar o ZFC no CIC, no qual o Coq se baseia.
Benjamin Werner: Conjuntos em Tipos, Tipos em Conjuntos (1997). http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709
[Isabelle] Existe uma biblioteca para a ZF.
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/index.html
fonte
Movido de comentário por sugestão de Kaveh
Primeiro, você precisa selecionar um assistente de prova. Coq é o que eu uso, mas existem muitos outros . Coq é baseado em lógica de ordem superior (o chamado Cálculo de Construções Indutivas). Outros assistentes de prova são baseados na lógica de primeira ordem, portanto podem ser mais adequados às suas necessidades (modulo os comentários acima).
Então você precisa se comprometer em aprender o assistente de prova. O documento vinculado é um tutorial para conhecer o Coq. Tornar-se um especialista em Coq requer anos de dedicação e prática, mas teoremas simples podem ser comprovados em uma tarde. A chave para aprender Coq ou qualquer outro assistente de prova é fazer provas, como as do artigo vinculado. Apenas ler o artigo ajudará muito pouco, porque toda a experiência de interagir com o assistente de prova não pode ser bem transmitida no papel.
Dentro de alguns dias, você poderá codificar teoremas simples, como o descrito acima, e prová-los. Não espere que faremos isso por você. Você não aprenderá nada dessa maneira.
Quando você conseguir provar esses teoremas, sinta-se à vontade para postar suas respostas aqui e talvez deixe alguns comentários sobre suas experiências.
Você está pronto para o desafio?
fonte
Existem muitos artigos de matemática escritos usando o assistente de provas Mizar: http://mizar.org/fm/
fonte
Dave Clarke sugere Coq, mas Isabelle realmente parece uma idéia muito melhor, já que possui uma biblioteca A para a ZF . Isabelle também é muito madura e inclui uma grande variedade de táticas e extensões.
Eu não usei pessoalmente o Mizar, mas também pode ser bom.
fonte
Em Isabelle / ZF você pode escrever algo como isto
Como você pode ver, Isabelle prova isso automaticamente. Claro que você pode escrever uma prova mais detalhada, se realmente quiser.
fonte
Esse mesmo teorema é um exemplo trabalhado (consulte o Exemplo 11) no tutorial incluído no meu software DC Proof 2.0. Faça o download gratuitamente no meu site http://www.dcproof.com
fonte