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.
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.