Difference between revisions of "Uma lista de Ferramentas para o Ensino de Lógica"

From Logic Wiki
Jump to navigation Jump to search
Line 344: Line 344:
  
 
<references>
 
<references>
<ref name='asl'>DITMARSCH, H. van. Logic courseware. 2010. A Comprehensive list of Tools for doing Logic. Association for Symbolic Logic. Disponível em: [http://www.ucalgary.ca/aslcle/logic-courseware/]. </ref>
+
<ref name="asl">DITMARSCH, H. van. Logic courseware. 2010. A Comprehensive list of Tools for doing Logic. Association for Symbolic Logic. Disponível em: [http://www.ucalgary.ca/aslcle/logic-courseware/]. </ref>
<ref name='wiedijk'>WIEDIJK, F. Digital Math by Categories with Samples. 2007. A compiled list of 300 Tools sorted by implementation, interaction, supported logic and size effort. Disponível em: [http://www.cs.ru.nl/freek/digimathbycategory.html].</ref>
+
<ref name="wiedijk">WIEDIJK, F. Digital Math by Categories with Samples. 2007. A compiled list of 300 Tools sorted by implementation, interaction, supported logic and size effort. Disponível em: [http://www.cs.ru.nl/freek/digimathbycategory.html].</ref>
 
</references>
 
</references>

Revision as of 21:04, 27 May 2013


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[1] e também a lista de Freek Wiedijk[2] com 300 ferramentas computacionais de aplicações e ensino de Lógica.



Akka

Criador e Editor de Modelos de Kripke. Foi desenvolvido em Java. [4]

Avaliação: -

Última atualização: -

Problemas: -


Alfie

É um programa editor de demonstrações em lógica proposicional. Tem a vantagem de apresentar a demonstração tal como um programa em Haskell. [5]

Avaliação: -

Última atualização: -.

Problemas: -

AproS

Um projeto que consiste em quatro sistemas integrados um mecanismo de busca de demonstrações Proof Generator, Proof Tutor, Proof Lab e curso web Logic & Proofs. É desenvolvido em Java Web Start. [6]

Avaliação: -

Última atualização: -

Problemas: -


ASA-CalcPro

É um ambiente de suporte ao aluno para o ensino-aprendizagem de cálculo proposicional. [7]

Avaliação: -

Última atualização: -

Problemas: -

Bertrand

Symbolic Logic Problem-Solving Software: Resolve conjuntos proposições de primeira ordem no que diz respeito a consistência, validade e equivalência. Classifica verdades lógicas e falsidades lógicas, e constrói tabelas de verdade. [8]

Avaliação: -

Última atualização: -

Problemas: -


BOP

Ferramenta educativa desenvolvida em Java para demonstrações à la Fitch da Delft university. [9]

Avaliação: -

Última atualização: -

Problemas: -


Computational Aristotelian Term Logic

Site dedicado aos aspectos formais da lógica aristotélica tradicional. Desenvolvido em PHP. [10]

Avaliação: -

Última atualização: -

Problemas: -


Coq

É um assistente de demonstrações formais, permite definir funções ou predicados, estabelecer teoremas matemáticos e especificações de softwares, desenvolver demonstrações formais interativamente e verificar estas demonstrações a partir de uma teoria formal. [11]

Avaliação: -

Última atualização: -

Problemas: -


Expression Evaluator Page

Analisador de expressões booleanas, com quantificadores e predicados. É um programa em CGI escrito em Perl. [12]

Avaliação: -

Última atualização: -

Problemas: -


Genie

É um ambiente de desenvolvimento para construção de modelos gráficos de decisões teóricas. [13]

Avaliação: -

Última atualização: 1999.

Problemas: Desatualizado.


Introdutory Logic Animations

Iniciativa idealizada e desenvolvida em 1999 por Jan Jaspars, contém programas em JavaScript para aprendizado interativo de lógica matemática básica. Implementa [14] aspectos como

  • Lógica proposicional e de primeira ordem: constrói modelos, contra-modelos, tabelas de verdade, avalia fórmulas e encontra instâncias para variáveis livres;
  • Lógica Modal: Calcula mundos dado um modelo e constrói mundos possíveis;
  • Lógica Dinâmica: Calcula a transação de uma expressão regular dada;
  • Simulação Máquinas de Turing.


Avaliação:[Muito bom]

Última atualização: 1999.

Problemas: Desatualizado.


Jape - Just Another Proof Editor

É um sistema desktop para prática de demonstrações de dedução natural. Bastante interessante e flexível que possibilita definir novas formalizações lógicas. [15]

Avaliação:[Muito bom]

Última atualização: 2012.

Problemas: -


Logic in Action

Trata-se da continuidade da iniciativa do projeto \ep{Introdutory Logic Animations de Jan Jaspars para o ensino de Lógica em cursos introdutórios e intermediários. O projeto disponibiliza materiais de aula, slides em inglês e espanhol, e programas interativos para ensinar Lógica Proposicional, Raciocínio Silogístico, Lógica de Primeira Ordem, Lógica Epistêmica, Lógica Dinâmica, Jogos Lógicos, Testes de Validade, Demonstrações e Método de Resolução. [16]

Avaliação:[Muito bom]

Última atualização: 2013.

Problemas: Programas não funcionam, estão com endereços quebrados.


LoTREC

Trata-se de uma ferramenta para a demonstração através do método de Tableau para Lógica de $1ª$ Ordem e Lógica Modal, implementada em Java e executável via Java Web Start. [17]

Avaliação: [Muito bom]

Última atualização: 2013.

Problemas: -

Modal Logic Playground

Trata-se de um avaliador de fórmulas e de relações de acessibilidade para a Lógica Modal Proposicional. Foi desenvolvido através da biblioteca JavaScript D3[3], MathJax[4] e o Twitter Bootstrap[5]. A ferramenta possui código livre disponível em [18]. [19]

Avaliação:[Muito bom]

Última atualização: 2013

  1. Cite error: Invalid <ref> tag; no text was provided for refs named asl
  2. Cite error: Invalid <ref> tag; no text was provided for refs named wiedijk
  3. Uma biblioteca JavaScript para manipulação de documentos a partir de seus dados. Disponível em [1].
  4. Uma biblioteca JavaScript para visualização de notações matemáticas. Disponível em [2].
  5. Uma framework para desenvolvimento de interfaces web. Disponível em [3].


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

  • 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. [21]

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 [22]

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


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

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

Avaliação: -

Última atualização: -

Problemas: -


The Daemon Proof Checker

Um verificador de demonstrações e de contramodelos. [26]

Avaliação: -

Última atualização: -

Problemas: -


Theorem Proving System

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

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


Tableau3

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


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

References

Cite error: <ref> tag defined in <references> has group attribute "" which does not appear in prior text.
Cite error: <ref> tag defined in <references> has group attribute "" which does not appear in prior text.