Na ciência da computação e na lógica matemática, um assistente de prova ou provador de teoremas interativo é uma ferramenta de software para auxiliar no desenvolvimento de provas formais por meio da colaboração homem-máquina. Isto envolve algum tipo de editor de provas interativo, ou outra interface, com a qual um ser humano pode orientar a busca por provas, cujos detalhes são armazenados e algumas etapas fornecidas por um computador. Neste artigo, você conhecerá 5 dos melhores assistentes de prova gratuitos e de código aberto para Linux.
Os assistentes
Este tipo de software fornece uma linguagem formal para escrever definições matemáticas, algoritmos executáveis ??e teoremas juntamente com um ambiente para desenvolvimento semi-interativo de provas verificadas por máquina. Eles auxiliam no desenvolvimento de provas formais por meio da colaboração homem-máquina. Eles oferecem uma linguagem formal onde coexistem definições matemáticas, algoritmos executáveis ??e teoremas, e um ambiente interativo que mantém o status atual da prova e a atualiza de acordo com comandos (geralmente chamados de táticas) emitidos pelo usuário.
Notícias Relacionadas
Futuro incerto para o BcacheFS
Debates acalorados: a suspensão de Kent Overstreet e as reações da comunidade
A suspensão temporária de Kent Overstreet, criador do BcacheFS, provocou uma avalanche de reações na comunidade Linux. Com opiniões divididas, desenvolvedores e membros da comunidade discutem sobre o impacto de suas ações e as consequências para o futuro do projeto no kernel Linux. O desenvolvedor suspenso também comentou em seu blog como tudo aconteceu. Comentários […]
Kent Overstreet
Kent Overstreet comenta suspensão em seu blog
Kent Overstreet, desenvolvedor da inovadora sistema de arquivos BcacheFS, enfrenta um momento delicado em sua carreira como contribuidor do kernel Linux. Sua suspensão temporária pelo comitê de Código de Conduta (CoC) gerou controvérsias sobre a forma como conflitos são geridos dentro da comunidade e levantou questões sobre os processos culturais e técnicos que guiam o […]
Abaixo, uma lista com 5 dos melhores assistentes de prova gratuitos e de código aberto, elaborada pelo pessoal do Linux Links.
Assistentes de prova
- Coq: Coq é um sistema formal de gerenciamento de provas. Ele fornece uma linguagem formal para escrever definições matemáticas, algoritmos executáveis ??e teoremas, juntamente com um ambiente para desenvolvimento semiinterativo de provas verificadas por máquina;
- Isabelle: Assistente de prova genérico; expressar fórmulas matemáticas em uma linguagem formal. Ele permite que fórmulas matemáticas sejam expressas em uma linguagem formal e fornece ferramentas para provar essas fórmulas em um cálculo lógico. A principal aplicação é a formalização de provas matemáticas e, em particular, a verificação formal, que inclui a comprovação da exatidão de hardware ou software de computador e a comprovação de propriedades de linguagens e protocolos de computador;
- Agda: Sistema interativo para redação e verificação de provas. Embora o Agda não tenha uma linguagem tática separada, é possível programar táticas úteis dentro do próprio Agda;
- Lean: Linguagem de programação e provador de teoremas. A biblioteca matemática Lean, mathlib, é um esforço conduzido pela comunidade para construir uma biblioteca unificada de matemática formalizada no assistente de prova Lean;
- Matita: Provador de teoremas experimental e interativo. Um provador interativo é uma ferramenta de software que auxilia no desenvolvimento de provas formais por meio da colaboração homem-máquina. Ele fornece uma linguagem formal onde coexistem definições matemáticas, algoritmos executáveis ????e teoremas, e um ambiente interativo que mantém o status atual da prova e a atualiza de acordo com comandos (geralmente chamados de táticas) emitidos pelo usuário.
