Difference between revisions of "Uma lista de Ferramentas para o Ensino de Lógica"
(Created page with " 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 ...") |
|||
| (17 intermediate revisions by the same user not shown) | |||
| Line 4: | Line 4: | ||
Listamos aqui uma seleção de softwares para o Ensino de Lógica com suas respectivas descrições. | 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 e também a lista de | + | Além de nossa lista, há uma lista mantida pelo grupo da Association for Symbolic Logic<ref name="asl"/> e também a lista de Freek Wiedijk<ref name="wiedijk"/> com 300 ferramentas computacionais de aplicações e ensino de Lógica. |
| Line 12: | Line 12: | ||
| − | Criador e Editor de Modelos de Kripke. Foi desenvolvido em Java. | + | Criador e Editor de Modelos de Kripke. Foi desenvolvido em Java. [http://staff.science.uva.nl/~lhendrik/AkkaStart.html] |
| − | |||
| − | |||
Avaliação: - | Avaliação: - | ||
| Line 25: | Line 23: | ||
== Alfie == | == 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. [http://www.cs.chalmers.se/~sydow/alfie/index.html] | |
| − | |||
| − | |||
| − | |||
Avaliação: - | Avaliação: - | ||
| Line 35: | Line 30: | ||
Problemas: - | Problemas: - | ||
| − | |||
== AproS == | == 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. | + | 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. [http://www.phil.cmu.edu/projects/apros/] |
| − | |||
| − | |||
Avaliação: - | Avaliação: - | ||
| Line 54: | Line 46: | ||
| − | É um ambiente de suporte ao aluno para o ensino-aprendizagem de cálculo proposicional. | + | É um ambiente de suporte ao aluno para o ensino-aprendizagem de cálculo proposicional. [http://www.asacalcpro.com.br/GiacomoN/index.htm] |
| − | |||
| − | |||
Avaliação: - | Avaliação: - | ||
| Line 63: | Line 53: | ||
Problemas: - | Problemas: - | ||
| − | |||
== Bertrand == | == 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. | + | 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. [http://www.uwosh.edu/faculty_staff/herzberg/Bertrand.html] |
| − | |||
| − | |||
Avaliação: - | Avaliação: - | ||
| Line 82: | Line 69: | ||
| − | Ferramenta educativa desenvolvida em Java para demonstrações à la Fitch da Delft university. | + | Ferramenta educativa desenvolvida em Java para demonstrações à la Fitch da Delft university. [http://dutiih.twi.tudelft.nl/~sicco/] |
| − | |||
| − | |||
Avaliação: - | Avaliação: - | ||
| Line 97: | Line 82: | ||
| − | Site dedicado aos aspectos formais da lógica aristotélica tradicional. Desenvolvido em PHP. | + | Site dedicado aos aspectos formais da lógica aristotélica tradicional. Desenvolvido em PHP. [http://logic.glashoff.net/aristotelianlogic/] |
| − | |||
| − | |||
Avaliação: - | Avaliação: - | ||
| Line 113: | Line 96: | ||
| − | É 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. | + | É 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. [http://pauillac.inria.fr/coq/] |
| − | |||
| − | |||
Avaliação: - | Avaliação: - | ||
| Line 127: | Line 108: | ||
| − | Analisador de expressões booleanas, com quantificadores e predicados. É um programa em CGI escrito em Perl. | + | Analisador de expressões booleanas, com quantificadores e predicados. É um programa em CGI escrito em Perl. [http://www.cc.utah.edu/~nahaj/logic/evaluate/] |
| − | |||
| − | |||
Avaliação: - | Avaliação: - | ||
| Line 143: | Line 122: | ||
| − | É um ambiente de desenvolvimento para construção de modelos gráficos de decisões teóricas. | + | É um ambiente de desenvolvimento para construção de modelos gráficos de decisões teóricas. [http://www2.sis.pitt.edu/~genie/] |
| − | |||
| − | |||
Avaliação: - | Avaliação: - | ||
| Line 159: | Line 136: | ||
| − | 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 aspectos | + | 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 [http://staff.science.uva.nl/~jaspars/animations/] 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] | Avaliação:[Muito bom] | ||
| Line 183: | Line 160: | ||
| − | É 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. | + | É 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. [http://www.cs.ox.ac.uk/people/bernard.sufrin/jape.html] |
| − | |||
| − | |||
Avaliação:[Muito bom] | Avaliação:[Muito bom] | ||
| Line 198: | Line 173: | ||
| − | 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. | + | 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. [http://www.logicinaction.org/] |
| − | |||
| − | |||
Avaliação:[Muito bom] | Avaliação:[Muito bom] | ||
| Line 213: | Line 186: | ||
| − | 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. | + | 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. [http://www.irit.fr/Lotrec/] |
| − | |||
| − | |||
Avaliação: [Muito bom] | Avaliação: [Muito bom] | ||
| Line 222: | Line 193: | ||
Problemas: - | Problemas: - | ||
| − | |||
== Modal Logic Playground == | == 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<ref name="d3"/>, MathJax<ref name="mj"/> e o Twitter Bootstrap<ref name="tb"/>. A ferramenta possui código livre disponível em | + | 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<ref group="modal" name="d3"/>, MathJax<ref group="modal" name="mj"/> e o Twitter Bootstrap<ref group="modal" name="tb"/>. A ferramenta possui código livre disponível em [https://github.com/rkirsling/modallogic]. [http://rkirsling.github.io/modallogic/] |
| − | |||
| − | |||
Avaliação:[Muito bom] | Avaliação:[Muito bom] | ||
| Line 235: | Line 203: | ||
Última atualização: 2013 | Última atualização: 2013 | ||
| − | <references> | + | <references group="modal"> |
<ref name="d3"> | <ref name="d3"> | ||
| − | Uma biblioteca JavaScript para manipulação de documentos a partir de seus dados. Disponível em | + | Uma biblioteca JavaScript para manipulação de documentos a partir de seus dados. Disponível em [http://d3js.org/]. |
</ref> | </ref> | ||
<ref name="mj"> | <ref name="mj"> | ||
| − | Uma biblioteca JavaScript para visualização de notações matemáticas. Disponível em | + | Uma biblioteca JavaScript para visualização de notações matemáticas. Disponível em [http://www.mathjax.org/]. |
</ref> | </ref> | ||
<ref name="tb"> | <ref name="tb"> | ||
| − | Uma framework para desenvolvimento de interfaces web. Disponível em | + | Uma framework para desenvolvimento de interfaces web. Disponível em [http://twitter.github.io/bootstrap/]. |
</ref> | </ref> | ||
</references> | </references> | ||
| − | |||
== Tarski's World, Fitch & Boole == | == 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. | + | 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. [http://ggww2.stanford.edu/GUS/lpl/] |
* '''Tarski's World''': ensina as bases da linguagem de primeira ordem e sua semântica; | * '''Tarski's World''': ensina as bases da linguagem de primeira ordem e sua semântica; | ||
| Line 259: | Line 226: | ||
* '''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. | * '''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: - | Avaliação: - | ||
| Line 271: | Line 238: | ||
| − | (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. | + | (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. [http://www.doc.ic.ac.uk/pandora/] |
| − | |||
| − | |||
Avaliação: - | Avaliação: - | ||
| Line 284: | Line 249: | ||
== Plato == | == 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 [http://www.utexas.edu/courses/plato/] | |
| − | |||
| − | |||
| − | |||
Avaliação: - | Avaliação: - | ||
| Line 294: | Line 256: | ||
Problemas: - | Problemas: - | ||
| − | |||
== Possible World Creation == | == Possible World Creation == | ||
| − | Analisa fórmulas modais a partir de um modelo de Kripke construído pelo usuário. | + | Analisa fórmulas modais a partir de um modelo de Kripke construído pelo usuário. [http://staff.science.uva.nl/~jaspars/lvi98/Week3/modal.html] |
| − | |||
| − | |||
| Line 307: | Line 266: | ||
| − | É 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. | + | É 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. [http://proofweb.cs.ru.nl/] |
| − | |||
| − | |||
Avaliação: - | Avaliação: - | ||
| Line 322: | Line 279: | ||
| − | É um verificador de demonstrações útil para busca de estratégias de demonstrações. E um verificador da correção de tableaux semântico. | + | É um verificador de demonstrações útil para busca de estratégias de demonstrações. E um verificador da correção de tableaux semântico. [http://selfpace.uconn.edu/BertieTwootie/software.htm] |
| − | |||
| − | |||
Avaliação: - | Avaliação: - | ||
| Line 336: | Line 291: | ||
| − | Um verificador de demonstrações e de contramodelos. | + | Um verificador de demonstrações e de contramodelos. [http://logic.tamu.edu/] |
| − | |||
| − | |||
Avaliação: - | Avaliação: - | ||
| Line 350: | Line 303: | ||
| − | É um sistema educacional demonstrador de teoremas desenvolvido em Common Lisp. | + | É um sistema educacional demonstrador de teoremas desenvolvido em Common Lisp. [http://gtps.math.cmu.edu/tps.html] |
| − | |||
| − | http://gtps.math.cmu.edu/tps.html | ||
Avaliação: - | Avaliação: - | ||
| Line 365: | Line 316: | ||
| − | É um aplicação que constroí tabelas de verdade para lógica proposicional. Desenvolvido em Java Applet's. | + | É um aplicação que constroí tabelas de verdade para lógica proposicional. Desenvolvido em Java Applet's. [http://www.brian-borowski.com/Software/Truth/] |
| − | |||
| − | |||
| Line 374: | Line 323: | ||
| − | + | Construtor de Tableaux desenvolvido em Java Applet's. [http://logic.philosophy.ox.ac.uk/tableau3/install.htm] | |
| − | Construtor de Tableaux desenvolvido em Java Applet's. | ||
| Line 385: | Line 333: | ||
| − | |||
| Line 391: | Line 338: | ||
| − | 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. | + | 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. [http://logicae.usal.es/mambo/index.php?option=com_summalogicaexxi&menu_task=Software&task=no_task&cmd=listar] |
| − | + | ==References== | |
| − | + | <references> | |
| − | DITMARSCH, H. van. Logic courseware. 2010. | + | <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> |
| − | /aslcle/logic-courseware/ | + | <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/digimath/bycategory.html].</ref> |
| − | + | </references> | |
| − | |||
| − | |||
| − | WIEDIJK, F. | ||
Latest revision as of 21:20, 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.
Contents
- 1 Akka
- 2 Alfie
- 3 AproS
- 4 ASA-CalcPro
- 5 Bertrand
- 6 BOP
- 7 Computational Aristotelian Term Logic
- 8 Coq
- 9 Expression Evaluator Page
- 10 Genie
- 11 Introdutory Logic Animations
- 12 Jape - Just Another Proof Editor
- 13 Logic in Action
- 14 LoTREC
- 15 Modal Logic Playground
- 16 Tarski's World, Fitch & Boole
- 17 Pandora
- 18 Plato
- 19 Possible World Creation
- 20 ProofWeb
- 21 The Bertie & Twootie
- 22 The Daemon Proof Checker
- 23 Theorem Proving System
- 24 Truth Table Constructor
- 25 Tableau3
- 26 Summa Logicae XXI
- 27 References
Akka
Criador e Editor de Modelos de Kripke. Foi desenvolvido em Java. [6]
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. [7]
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. [8]
Avaliação: -
Última atualização: -
Problemas: -
ASA-CalcPro
É um ambiente de suporte ao aluno para o ensino-aprendizagem de cálculo proposicional. [9]
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. [10]
Avaliação: -
Última atualização: -
Problemas: -
BOP
Ferramenta educativa desenvolvida em Java para demonstrações à la Fitch da Delft university. [11]
Avaliação: -
Última atualização: -
Problemas: -
Computational Aristotelian Term Logic
Site dedicado aos aspectos formais da lógica aristotélica tradicional. Desenvolvido em PHP. [12]
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. [13]
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. [14]
Avaliação: -
Última atualização: -
Problemas: -
Genie
É um ambiente de desenvolvimento para construção de modelos gráficos de decisões teóricas. [15]
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 [16] 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. [17]
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. [18]
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. [19]
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[modal 1], MathJax[modal 2] e o Twitter Bootstrap[modal 3]. A ferramenta possui código livre disponível em [20]. [21]
Avaliação:[Muito bom]
Última atualização: 2013
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. [22]
- 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. [23]
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 [24]
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. [25]
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. [26]
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. [27]
Avaliação: -
Última atualização: -
Problemas: -
The Daemon Proof Checker
Um verificador de demonstrações e de contramodelos. [28]
Avaliação: -
Última atualização: -
Problemas: -
Theorem Proving System
É um sistema educacional demonstrador de teoremas desenvolvido em Common Lisp. [29]
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. [30]
Tableau3
Construtor de Tableaux desenvolvido em Java Applet's. [31]
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. [32]
References
- ↑ DITMARSCH, H. van. Logic courseware. 2010. A Comprehensive list of Tools for doing Logic. Association for Symbolic Logic. Disponível em: [4].
- ↑ 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: [5].
