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. [3]

• 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.

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. [10]

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. [11]

Tableau3

Construtor de Tableaux desenvolvido em Java Applet's. [12]

Avaliação:[Regular]

Última atualização: 2005.

Problemas: Desatualizados. Aplicações Desktop.

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. [13]