PROGRAMAS E MANUAIS

Versão mais recente: 7.0 d 14
Página oficial do Jape: http://www.cs.ox.ac.uk/people/bernard.sufrin/jape.html
Onde baixar a versão atual: http://www.cs.ox.ac.uk/people/bernard.sufrin/BUILDS/v7_d14/

Manuais:

Na página oficial, não há manual específico para a versão mais recente, que difere das mais antigas nos menus, nas janelas e em comportamento durante as provas. Porém, é possível se guiar através deles. Estes são encontrados na seção "Manuals".

O primeiro da lista, "Roll Your Own Jape Logic", é uma descrição das várias lógicas aceitas pelo Jape, exemplos de provas e como modificar o Jape (menus, botões, regras de inferências, conjecturas, etc). É necessário apenas para quem quer entender com mais profundidade o funcionamento e as lógicas que o Jape suporta.

O segundo deles "Manual on forward reasoning", mostra como fazer sua codificação para o Jape usar uma determinada lógica aplicar passos para a frente.

O terceiro, "Natural Deduction manual", explica como usar a teoria de dedução natural que vem com o Jape, mostrando como provar e desprovar conjecturas.

Por fim, o quarto, "Disproof manual", explica como provar que uma conjectura é falsa usando diagramas de Kripke.

Na sessão seguinte, "Resources", também há outros documentos e links interessantes.

INSTALAÇÃO NO LINUX

1. Não foi testado para a versão mais recente, estou apenas reproduzindo alguns passos que certamente serão utilizados;
   
   
2. No X-Windows, abra uma janela do terminal;
   
   
3. Vá para o diretório onde o arquivo InstallLinuxjape.jar está localizado;
   
   
4. Execute o comando javaw -jar InstallLinuxjape.jar;
   
   
5. Aperte o botão para instalar o Jape, e
   
   
6. Feche o programa instalador;
   
   

INSTALAÇÃO NO WINDOWS

1. Execute o arquivo InstallWindowsjape.jar dando um clique duplo nele;
   
   
2. Alternativamente, abra o prompt de comando onde está o jar (usando SHIFT e botão direito do mouse e escolhendo "Abrir janela de comando aqui"), e execute o comando javaw -jar InstallWindowsjape.jar;
   
   
3. Se desejar instalar o Jape em outro diretório diferente do da localidade do jar, edite o caminho em "Install to" ou escolha outro em "Choose Installation Folder";
   
   
4. Aperte o botão "Install" para instalar o Jape;
   
   
5. Feche o programa instalador em "Exit (and clean up) Now"; e
   
   
6. Se tiver marcado a opção "Shortcut on Desktop", ela não funcionará corretamente no Windows 8 pelo fato de não haver o arquivo C:\WINDOWS\system32\javaw.exe. Se quiser usar o atalho no desktop nessa versão de Windows, edite-o para usar o link do javaw.exe da sua instalação do Java.
   
   

ESCOLHENDO UMA TEORIA NO JAPE

1. Vá ao diretório onde o Jape foi instalado e dê um clique duplo em Jape.jar ou execute o comando javaw -jar Jape.jar;
   
   
2. Vá ao menu "file" e selecione a opção: "Open new theory...";
   
   
3. Para trabalhar com os exemplos, vá para o diretório "examples" do Jape. Senão, escolha um diretório onde há um arquivo de teoria;
   
   
4. Selecione o tipo de lógica com o qual quer trabalhar dando dois cliques na selecionada (cada um tem seu sub-diretório em examples);
   
   
5. Abra o arquivo com a teoria desejada, que tem a extensão .jt; e
   
   
6. Se tiver salvo provas para conjecturas desta mesma teoria (arquivo .jp), abrá-as, pois as já provadas podem ser utilizadas como teoremas (quando uma prova estiver em andamento, selecione o teorema desejado e pressione "Apply").
   
   
   

PROVANDO UMA CONJECTURA JAPE

1. Para tentar provar uma conjectura, selecione uma em uma das janelas de conjecturas abertos na teoria;
   
   
2. Aperte o botão "Prove" na janela onde se localiza a conjectura;
   
   
3. Uma nova janela é aberta, onde se prova uma conjectura;
   
   
4. Ao terminar de provar a conjectura (se isso for possível) não mais haverá ... em certos pontos de sua prova. Também, a entrada "Done" do menu "Edit" estará habilitada;
   
   
5. Ao selecionar "Done", a prova será apagada da janela principal do Jape e no painel de conjecturas onde está a conjectura selecionada, do lado esquerdo da provada, estará um "tick", já que foi provada;
   
   
6. Se suspeitar de que a conjectura é inválida, tente disprová-la utilizando a entrada "Disprove" do menu "Edit". Tendo feito isso, "Done" também estará habilitado. Neste caso, ao selecionar esta entrada do menu, a prova será apagada da janela principal do Jape e no painel de conjecturas onde está a conjectura selecionada, do lado esquerdo da que não pode ser provada, estará um "x", indicando que é inválida, já que não pode ser provada;
   
   
7. Apertando-se o botão "Show Proof" na janela de conjecturas e selecionando a conjectura provada, a prova dela é exibida na janela principal do Jape;
   
   
8. Para salvar a prova, selecione a entrada "Save Proofs" ou "Save Proofs As" do menu "File". Já para imprimi-la, selecione "Print" deste mesmo menu;
   
   
9. Durante uma prova, é possível retroceder e refazer seus passos utilizando as entradas "Undo" e "Redo", respectivamente, do menu "Edit";
   
   
10. Durante uma prova, será necessário selecionar uma ou mais fórmulas. Para selecionar uma prova, clique com um botão do mouse sobre ela. Para selecionar mais de uma, aperte o "SHIFT" e clique sobre a(s) outra(s) fórmula(s) desejada(s). Já para remover todas as seleções, clique fora da prova;
    
    
11. Também pode se desejar selecionar parte de uma fórmula. Para isso, use o botão do meio e arraste-o sobre a sub-fórmula desejada até que toda ela fique selecionada. Para remover a seleção, clique fora da prova, e
    
    
12. Se quiser provar uma conjectura que não esteja em nenhuma janela, escolha a janela desejada e pressione o botão "New". Aparecerá uma nova janela. Nesta, edite sua conjectura. Ao terminar, pressione a tecla "Enter" e a nova conjectura estará na janela desejada.
    
    

TRABALHANDO COM DEDUÇÃO NATURAL NO JAPE

1. Selecione natural_deduction no passo 3 de "ESCOLHENDO UMA TEORIA NO JAPE". Na pasta há duas teorias. Escolha I2L.jt;
   
   
2. 3 janelas serão abertas: a de conjecturas clássicas (onde é necessária a regra de redução ao absurdo clássico para a conclusão das provas), a de conjecturas inválidas (que não podem ser provadas) e a de conjecturas;
   
   
3. Na dedução natural, o Jape vem configurado apenas para exibir a prova linearmente, e não em árvore. Para poder fazer esta escolha, é necessário editar os arquivos que compõem a teoria de dedução natural. Para fazer isso, leia o manual "Roll Your Own Jape Logic", que mostra como adicionar entradas aos menus; e
   
   
4. Na teoria de dedução natural, dois menus aparecem na janela de prova de uma conjectura: "Backward" (para manipular uma conclusão em uma prova) e "Forward" (para manipular uma premissa em uma prova).
   
   

EXEMPLOS DE PROVAS EM DEDUÇÃO NATURAL NO JAPE

Primeiro Exemplo:

1. Escolha a seguinte conjectura do painel de conjecturas ("Conjectures"): Ø E |- E ® F;
   
   
2. Aperte "Prove" na janela onde ela se encontra. Observe que a premissa e a conclusão estão na tela, com ... indicando a prova que falta para demonstrar a conclusão a partir da premissa;
   
   
3. Selecione E ® F (linha 2), vá no menu "Backward" e escolha a regra ® intro, que significa introdução da implicação;
   
   
4. Feito isso, selecione Ø E (linha 1) e E (linha 2), vá ao menu "Forward" e escolha a regra Ø elim, que significa eliminação da negação;
   
   
5. Agora, selecione F (linha 4), vá ao menu "Backward" e escolha a regra contra (construtive), que significa absurdo intucionista; e
   
   
6. A prova está completa! Eis as provas completas:
   
   

   Formato linear

   Formato em árvore

Segundo Exemplo:

1. Escolha a seguinte conjectura do painel de conjecturas clássicas ("Classical conjectures"): Ø"x.R(x) |- $x.ØR(x);
   
   
2. Aperte "Prove" na janela onde ela se encontra e vá para a nova janela;
   
   
3. Selecione $x.ØR(x) (linha 2), vá ao menu "Backward" e escolha a regra contra (classical), que significa absurdo clássico;
   
   
4. Feito isso, selecione Ø"x.R(x) (linha 1) e ^ (linha 3), vá ao menu "Forward" e escolha a regra Ø elim;
   
   
5. Agora, selecione "x.R(x) (linha 3), vá ao menu "Backward" e escolha a regra " intro, que significa introdução do para todo;
   
   
6. Selecione R(i) (linha 4), vá ao menu "Backward" e escolha a regra contra (classical);
   
   
7. Feito isso, selecione Ø$x.ØR(x) (linha 2) e ^ (linha 5), vá ao menu " Backward" e escolha a regra Ø elim;
   
   
8. Agora, selecione actual i (linha 3) e $x.ØR(x) (linha 5), vá ao menu " Backward" e escolha a regra $ intro, que significa introdução do existe; e
   
   
9. A prova está completa! Eis as provas completas:
   
   

   Formato linear

   Formato em árvore

FACILIDADE PROVIDA PARA DEDUÇÃO NATURAL

A grande facilidade oferecida para provas em dedução natural (e em todas as outras teorias) é o fato de que o Jape não deixa o usuário fazer provas de maneira errada, ou seja, utilizar as regras de maneira errada, construindo provas incorretas e até mesmo provando conjecturas inválidas. Ao tentar fazer isso, será exibida uma mensagem de erro indicando o que está e o que não está correto no uso da regra (algo de muita utilidade!), e o que o usuário deveria fazer para usar adequadamente a mesma.

Obviamente, é possível fazer provas erradas se o usuário editar a teoria de dedução natural e acrescentar regras de inferência inválidas (ou modificar as atuais de modo a deixá-las incorretas).

DIFICULDADES NO USO DA DEDUÇÃO NATURAL

A maior dificuldade é que o Jape tem como padrão para dedução natural apenas provas feitas linearmente. Para quem está acostumado a fazer provas em árvore, muitas vezes é difícil entender o andamento da prova.

Outro problema é que ele não prova nada automaticamente em dedução natural. Para tentar fazer isso em outras teorias, clica-se duas vezes com o botão esquerdo do mouse em cima de uma fórmula. Se fosse possível, ele "andaria um passo" (e somente um) no processo de prova (pois é assim que acontece nas outras). Todavia, mesmos nessas, na maioria das vezes, ele dará mensagens de erro ou tentará caminhos ruins. No caso de dedução natural, ele simplesmente dá uma de mensagem de erro dizendo que o duplo clique nada significa para esta teoria. Concluindo, o Jape é mais um editor de provas do que um provador de teoremas.

Ainda, é complicado o uso das regras de eliminação e introdução dos quantificadores. Quando se faz isto no papel, usa-se constantes na hora de eliminar e inserir quantificadores e a única preocupação é com o uso correto das regras. Já no Jape, é necessário fazer "pseudo-hipóteses" sobre as variáveis que serão usadas com estas regras (não são constantes) e isto deve ser utilizado explicitamente durante as provas, como mostrado no último exemplo (a variável i).

EXERCÍCIOS DE DEDUÇÃO NATURAL

1. Prove, utilizando o Jape, as conjecturas nas janelas "Conjectures" e "Classical conjectures".
   
   
2. Prove, utilizando o Jape, outras conjecturas proposicionais (algumas bem difíceis) contidas neste arquivo. Para utilizá-lo, é só descompactá-lo e, após abrir a teoria de dedução natural no Jape ir em File -> Open... e abrir o arquivo outras_conj_prop.j.
   
   
3. Prove, utilizando o Jape, outras conjecturas em primeira ordem (não tão difíceis assim) contidas neste arquivo.