Descrição
Resolve fórmulas lógicas automaticamente usando técnicas de satisfatibilidade módulo teorias. Pesquisadores, engenheiros de verificação e desenvolvedores avançados usam esta ferramenta para checar provas, restrições, modelos e propriedades de programas.
É uma ferramenta especializada de linha de comando, não um aplicativo geral para aprender matemática. Use quando outro fluxo de verificação pedir CVC4 ou quando você trabalha diretamente com problemas de lógica formal.