Uma lista de Ferramentas para o Ensino de Lógica

Listamos aqui uma seleção de softwares para o Ensino de Lógica com suas respectivas descrições.

Além de nossa lista, há uma lista mantida pelo grupo da Association for Symbolic Logic </references>

Tarski's World, Fitch & Boole

São disponibilizados junto com o livro Language, Proof and Logic, compõem três programas desktop que implementam diferentes aspectos da lógica, a saber, Modelos Semânticos, demonstrações formais \ep{à la Fitch e Tabelas de Verdade.

• Tarski's World: ensina as bases da linguagem de primeira ordem e sua semântica;

• Fitch: um ambiente de assistência e verificação de dedução natural.

• Boole: um programa que facilita a construção e verificação de tabelas de verdade relacionando com suas principais noções de tautologia, consequência e equivalência.

[3]

Avaliação: -

Última atualização: -

Problemas: -

Pandora

(Proof Assistant for Natural Deduction using Organised Rectangular Areas): é uma ferramenta de aprendizado e suporte para a construção de demonstrações em dedução natural. Está disponível através de Java Applet's.

[4]

Avaliação: -

Última atualização: -

Problemas: -

Plato

É uma ferramenta para a construção de demonstrações em linguagens formais de cálculo sentencial, cálculo de predicados e teoria dos conjuntos.

[5]

Avaliação: -

Última atualização: -

Problemas: -

Possible World Creation

Analisa fórmulas modais a partir de um modelo de Kripke construído pelo usuário.

[6]

ProofWeb

É um sistema tanto para ensino de lógica e assistência de demonstrações na Web. É desenvolvido em PHP e serve como comunicação entre uma interface Web e o demonstrador de Teoremas Coq que funciona no servidor.

[7]

Avaliação: -

Última atualização: -

Problemas: -

The Bertie & Twootie

É um verificador de demonstrações útil para busca de estratégias de demonstrações. E um verificador da correção de tableaux semântico.

[8]

Avaliação: -

Última atualização: -

Problemas: -

The Daemon Proof Checker

Um verificador de demonstrações e de contramodelos.

[9]

Avaliação: -

Última atualização: -

Problemas: -

Theorem Proving System

É um sistema educacional demonstrador de teoremas desenvolvido em Common Lisp.

http://gtps.math.cmu.edu/tps.html]

Avaliação: -

Última atualização: -

Problemas: -

Truth Table Constructor

É um aplicação que constroí tabelas de verdade para lógica proposicional. Desenvolvido em Java Applet's.

[10]

Tableau3

Construtor de Tableaux desenvolvido em Java Applet's.

Avaliação:[Regular]

Última atualização: 2005.

Problemas: Desatualizados. Aplicações Desktop.

[11]

Summa Logicae XXI

Coletânea de diversos softwares relacionados com o ensino de lógica desenvolvidos em Java: DiagVenn1.0: Diagramas para lógica de predicados monádicos. MAFIA: Constrói tableaux proposicionais. Modelos de Kripke: Analisa fórmulas modais em modelos de Kripke definidos pelo usuário e verifica as propriedades de acessabilidade.Diagramas de Peirce: Permite a realização de um sistema para representação de gráficos. Possibilita o desenvolvimento em um sistema de gráficos de Peirce. Tradutor de lógicas: Ferramenta que proporciona um simulador gráfico de um tradutor de fórmulas em lógica modal para lógicas multivaloradas.

[12]