Changes

Jump to navigation Jump to search

Uma lista de Ferramentas para o Ensino de Lógica (view source)

Revision as of 15:04, 27 May 2013

10,099 bytes added ,  15:04, 27 May 2013
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 ..."



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.




== Akka ==


Criador e Editor de Modelos de Kripke. Foi desenvolvido em Java.

[[http://staff.science.uva.nl/~lhendrik/AkkaStart.html]]

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.

[[http://www.cs.chalmers.se/~sydow/alfie/index.html]]

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.

[[http://www.phil.cmu.edu/projects/apros/]]

Avaliação: -

Última atualização: -

Problemas: -



== ASA-CalcPro ==


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

[[http://www.asacalcpro.com.br/GiacomoN/index.htm

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.

[[http://www.uwosh.edu/faculty_staff/herzberg/Bertrand.html]]

Avaliação: -

Última atualização: -

Problemas: -


== BOP ==


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

[[http://dutiih.twi.tudelft.nl/~sicco/]]

Avaliação: -

Última atualização: -

Problemas: -



== Computational Aristotelian Term Logic ==


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

[[http://logic.glashoff.net/aristotelianlogic/]]

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.

[[http://pauillac.inria.fr/coq/]]

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.

[[http://www.cc.utah.edu/~nahaj/logic/evaluate/]]

Avaliação: -

Última atualização: -

Problemas: -



== Genie ==



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

[[http://www2.sis.pitt.edu/~genie/]]

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 aspectos de

- 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.

[[http://staff.science.uva.nl/~jaspars/animations/]]

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.

[[http://www.cs.ox.ac.uk/people/bernard.sufrin/jape.html]]

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.

[[http://www.logicinaction.org/]]

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.

[[http://www.irit.fr/Lotrec/]]

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<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/]]

Avaliação:[Muito bom]

Última atualização: 2013

<references>
<ref name="d3">
Uma biblioteca JavaScript para manipulação de documentos a partir de seus dados. Disponível em [[http://d3js.org/]].
</ref>
<ref name="mj">
Uma biblioteca JavaScript para visualização de notações matemáticas. Disponível em [[http://www.mathjax.org/]].
</ref>
<ref name="tb">
Uma framework para desenvolvimento de interfaces web. Disponível em [[http://twitter.github.io/bootstrap/]].
</ref>
</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.

[[http://ggww2.stanford.edu/GUS/lpl/]]

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.

[[http://www.doc.ic.ac.uk/pandora/]]

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.

[[http://www.utexas.edu/courses/plato/]]

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.

[[http://staff.science.uva.nl/~jaspars/lvi98/Week3/modal.html]]


== 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.

[[http://proofweb.cs.ru.nl/]]

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.

[[http://selfpace.uconn.edu/BertieTwootie/software.htm]]

Avaliação: -

Última atualização: -

Problemas: -


== The Daemon Proof Checker ==


Um verificador de demonstrações e de contramodelos.

[[http://logic.tamu.edu/]]

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.

[[http://www.brian-borowski.com/Software/Truth/]]



== Tableau3 ==



Construtor de Tableaux desenvolvido em Java Applet's.


Avaliação:[Regular]

Última atualização: 2005.

Problemas: Desatualizados. Aplicações Desktop.


[[http://logic.philosophy.ox.ac.uk/tableau3/install.htm]]


== 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.

[[http://logicae.usal.es/mambo/index.php?option=com_summalogicaexxi&menu_task=Software&task=no_task&cmd=listar]]


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/]].



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]].
Retrieved from "http://carol.dimap.ufrn.br/logicwiki/index.php/Special:MobileDiff/97"

Navigation menu