Material de apoio – JAPE (v7_d4_9)

1.  Java Runtime Environment

Para rodar o JAPE, é necessário primeiramente ter um JRE (Java Runtime Environment) instalado. Desta forma, o sistema operacional passa a contar com recursos da linguagem Java, e o JAPE pode ser executado independente da plataforma escolhida. A versão do JRE deve ser a 1.4 ou superior.

O download do JRE pode ser realizado no site www.javasoft.com.

2. Instalação do JAPE

A versão mais atual o JAPE (em Agosto de 2006) é a v7_d4_9. Para começar a utilizá-lo, faça o download no site http://jape.comlab.ox.ac.uk:8080/jape/BUILDS/v7_d4_9/ e, de acordo com o sistema operacional, selecione o arquivo desejado: InstallWindowsjape.jar para Windows ou InstallLinuxjape.jar  para Linux.

Com o download concluído, execute o programa InstallWindowsjape.jar (Windows). Quando aparecer a frase “The installer will clean up on exit”, clique no botão “Exit (and clean up) now”. Será criada a pasta “Jape” no local indicado (se o destino não for alterado, a pasta será criada no mesmo local do arquivo de instalação).

Para começar a utilizar o JAPE, execute o arquivo “Jape.jar”.

Vale lembrar novamente que se não houver o Java instalado então a aplicação não irá rodar. Não é necessário ter o JDK (Java Development Kit) completo, apenas o JRE conforme dito anteriormente.

3. Utilizando o JAPE

Para fazer uma prova utilizando dedução natural, por exemplo, selecione a opção do menu “File” e “Open New Theory...”. Na janela que se abrirá, escolha a pasta “examples”, depois a pasta “natural_deduction” e escolha um exemplo (I2L.jt).

Serão abertas três janelas, cada uma com conjecturas diferentes: as clássicas, que são provadas com a regra de redução ao absurdo, as inválidas, que não possuem prova válida, e as conjecturas.

Para seguir os passos da prova, utilize os itens Backward e Forward. No primeiro caso, a opção selecionada irá partir de uma conclusão e chegará ao seu desmembramento. No segundo caso, a opção desejada irá partir de uma (ou mais) premissa(s) para uma conclusão (final ou não).

4. Exemplo

Para entender melhor, siga os passos da seguinte prova:

•  Selecione a linha EvF, ~F |- E na janela de conjecturas;
•  Clique o botão “Prove”;
•  Selecione EvF (linha 1);
•  No menu, escolha a opção “v elim (makes assumptions)” no item Forward ;
•  Selecione ~F (linha 1) e F (linha 3);
•  No menu, escolha a opção “ ~ elim” também no item Forward ;
•  Selecione E (linha 5);
•  No menu, escolha a opção “contra (construtive)” no item Backward .

Com isso, será exibida a seguinte tela com o resultado da prova: