Coq – Provando teoremas de forma programática

O Coq é um “provador” de teoremas de maneira interativa. Ele nos auxilia a definir funções, predicados, a verificar as provas e suas consistências de maneira programática. Existem outras ferramentas que tem um propósito similar, como o Isabelle da Universidade Continue lendo Coq – Provando teoremas de forma programática

File not found e unknown option no latex

Para poder escrever minha qualificação no Latex, era necessário o pacote do abntex2. Entretanto não encontrei ele na minha distribuição linux, que no caso é o Gentoo. Após obter o seguinte erro: [sourcecode]File `abntex2.cls’ not found. ^^M[/sourcecode] Fiz uma busca Continue lendo File not found e unknown option no latex