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

From Logic Wiki
Jump to navigation Jump to search
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 Wiedijk2007} com 300 ferramentas computacionais de aplicações e ensino de Lógica.
+
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 14: Line 14:
 
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]]
+
[http://staff.science.uva.nl/~lhendrik/AkkaStart.html]
  
 
Avaliação: -
 
Avaliação: -
Line 27: Line 27:
 
É um programa editor de demonstrações em lógica proposicional. Tem a vantagem de apresentar a demonstração tal como um programa em Haskell.
 
É 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]]
+
[http://www.cs.chalmers.se/~sydow/alfie/index.html]
  
 
Avaliação: -
 
Avaliação: -
Line 39: Line 39:
 
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/]]
+
[http://www.phil.cmu.edu/projects/apros/]
  
 
Avaliação: -
 
Avaliação: -
Line 54: Line 54:
 
É 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]]
+
[http://www.asacalcpro.com.br/GiacomoN/index.htm]
  
 
Avaliação: -
 
Avaliação: -
Line 67: Line 67:
 
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]]
+
[http://www.uwosh.edu/faculty_staff/herzberg/Bertrand.html]
  
 
Avaliação: -
 
Avaliação: -
Line 81: Line 81:
 
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/]]
+
[http://dutiih.twi.tudelft.nl/~sicco/]
  
 
Avaliação: -
 
Avaliação: -
Line 96: Line 96:
 
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/]]
+
[http://logic.glashoff.net/aristotelianlogic/]
  
 
Avaliação: -
 
Avaliação: -
Line 112: Line 112:
 
É 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/]]
+
[http://pauillac.inria.fr/coq/]
  
 
Avaliação: -
 
Avaliação: -
Line 126: Line 126:
 
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/]]
+
[http://www.cc.utah.edu/~nahaj/logic/evaluate/]
  
 
Avaliação: -
 
Avaliação: -
Line 142: Line 142:
 
É 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/]]
+
[http://www2.sis.pitt.edu/~genie/]
  
 
Avaliação: -
 
Avaliação: -
Line 166: Line 166:
 
- Simulação Máquinas de Turing.
 
- Simulação Máquinas de Turing.
  
−
[[http://staff.science.uva.nl/~jaspars/animations/]]
+
[http://staff.science.uva.nl/~jaspars/animations/]
  
 
Avaliação:[Muito bom]
 
Avaliação:[Muito bom]
Line 182: Line 182:
 
É 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]]
+
[http://www.cs.ox.ac.uk/people/bernard.sufrin/jape.html]
  
 
Avaliação:[Muito bom]
 
Avaliação:[Muito bom]
Line 197: Line 197:
 
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/]]
+
[http://www.logicinaction.org/]
  
 
Avaliação:[Muito bom]
 
Avaliação:[Muito bom]
Line 212: Line 212:
 
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/]]
+
  [http://www.irit.fr/Lotrec/]
  
 
Avaliação: [Muito bom]
 
Avaliação: [Muito bom]
Line 224: Line 224:
  
  
−
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 [[https://github.com/rkirsling/modallogic]].
+
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 [https://github.com/rkirsling/modallogic].
  
−
[[http://rkirsling.github.io/modallogic/]]
+
[http://rkirsling.github.io/modallogic/]
  
 
Avaliação:[Muito bom]
 
Avaliação:[Muito bom]
Line 234: Line 234:
 
<references>
 
<references>
 
<ref name="d3">
 
<ref name="d3">
−
Uma biblioteca JavaScript para manipulação de documentos a partir de seus dados. Disponível em [[http://d3js.org/]].
+
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 [[http://www.mathjax.org/]].
+
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 [[http://twitter.github.io/bootstrap/]].
+
Uma framework para desenvolvimento de interfaces web. Disponível em [http://twitter.github.io/bootstrap/].
 
</ref>
 
</ref>
 
</references>
 
</references>
Line 256: Line 256:
 
* '''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.
  
−
[[http://ggww2.stanford.edu/GUS/lpl/]]
+
[http://ggww2.stanford.edu/GUS/lpl/]
  
 
Avaliação: -
 
Avaliação: -
Line 270: Line 270:
 
(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/]]
+
[http://www.doc.ic.ac.uk/pandora/]
  
 
Avaliação: -
 
Avaliação: -
Line 284: Line 284:
 
  É uma ferramenta para a construção de demonstrações em linguagens formais de cálculo sentencial, cálculo de predicados e teoria dos conjuntos.
 
  É 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/]]
+
[http://www.utexas.edu/courses/plato/]
  
 
Avaliação: -
 
Avaliação: -
Line 298: Line 298:
 
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]]
+
[http://staff.science.uva.nl/~jaspars/lvi98/Week3/modal.html]
  
  
Line 306: Line 306:
 
É 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/]]
+
[http://proofweb.cs.ru.nl/]
  
 
Avaliação: -
 
Avaliação: -
Line 321: Line 321:
 
É 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]]
+
[http://selfpace.uconn.edu/BertieTwootie/software.htm]
  
 
Avaliação: -
 
Avaliação: -
Line 335: Line 335:
 
Um verificador de demonstrações e de contramodelos.
 
Um verificador de demonstrações e de contramodelos.
  
−
[[http://logic.tamu.edu/]]
+
[http://logic.tamu.edu/]
  
 
Avaliação: -
 
Avaliação: -
Line 349: Line 349:
 
É 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 364: Line 364:
 
É 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/]]
+
[http://www.brian-borowski.com/Software/Truth/]
  
  
Line 382: Line 382:
  
  
−
[[http://logic.philosophy.ox.ac.uk/tableau3/install.htm]]
+
[http://logic.philosophy.ox.ac.uk/tableau3/install.htm]
  
  
Line 390: Line 390:
 
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]]
+
[http://logicae.usal.es/mambo/index.php?option=com_summalogicaexxi&menu_task=Software&task=no_task&cmd=listar]
  
 +
==References==
  
−
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-
+
<references>
−
/aslcle/logic-courseware/]].
+
<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/digimath/bycategory.html].
 +
</ref>
  
−
 
+
</references>
−
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]].
 

Revision as of 15:08, 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>


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.

Retrieved from "http://carol.dimap.ufrn.br/logicwiki/index.php?title=Uma_lista_de_Ferramentas_para_o_Ensino_de_Lógica&oldid=100"