Uma lista de Ferramentas para o Ensino de Lógica

From Logic Wiki
Revision as of 15:08, 27 May 2013 by Admin (talk | contribs)
Jump to navigation Jump to search


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 LogicCite error: Closing </ref> missing for <ref> tag [1] [2] </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]

References

  1. Uma biblioteca JavaScript para visualização de notações matemáticas. Disponível em [1].
  2. Uma framework para desenvolvimento de interfaces web. Disponível em [2].

Cite error: <ref> tag with name "asl" defined in <references> is not used in prior text.
Cite error: <ref> tag with name "wiedijk" defined in <references> is not used in prior text.