Difference between revisions of "Uma lista de Ferramentas para o Ensino de Lógica"
(→Plato) |
|||
| Line 344: | Line 344: | ||
<references> | <references> | ||
| + | |||
<ref name="asl"> | <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/]. | 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/]. | ||
Revision as of 15:53, 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 LogicCite error: Closing </ref> missing for <ref> tag
[1]
[2]
</references>
Contents
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]
References
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.
