Ferramentas de Apoio

PRINCIPAIS

• LogicTools

  • Site: http://logictools.org

  • Site completo com ferramentas de resolução para lógica proposicional.

• NuSMV

  • Site: http://nusmv.fbk.eu

  • Ferramenta para analisar especificações em lógica temporal.

• LogiText

  • Site: http://logitext.mit.edu/main

    • Provador de teoremas Estilo Gentzen - cálculo de sequents

• Fitch

  • Site: http://proofmood.com/en/Fitch/fitch.php

  • Verificador de regras de dedução natural.

• Babbage

  • Site: http://logica.stanford.edu/logica/php/babbage.php

  • Constrói tabelas-verdade a partir de fórmulas em lógica proposicional.

• Boole

  • Site: http://logica.stanford.edu/logica/php/boole.php

  • Mostra vinculação semântica através do método da tabela verdade, para fórmulas na lógica proposicional.

• Alloy Analyzer

  • Download:https://alloytools.org/

  • Ferramenta de modelagem simplificada baseada na lógica de primeira ordem.

OUTRAS (ADICIONAIS)

• • WinKE

  • Download: Está em arquivos, logo abaixo.

  • Recomendação: Ao baixar, mude a extensão do arquivo de 'z' para 'exe'. Descompacte o arquivo e instale a fonte winke.ttf para correta visualização da interface gráfica do aplicativo.

  • Página do autor: http://staff.science.uva.nl/~ulle/WinKE/

  • Descrição: WinKE é um assistente para provas interativas baseado no cálculo KE, um sistema de refutação que combina características dos tableaux analíticos de Smullyan com dedução natural de Gentze. O software foi concebido para servir como um sistema de tutoria para apoiar o ensino de lógica e raciocínio em um nível introdutório e vem sendo utilizado em cursos de Lógica, Inteligência Artificial e Filosofia em universidades de todo o mundo.

  • Tree Proof Generator

  • Aplicação Web: http://www.umsu.de/logik/trees/

  • Descrição: Formulário simples que tenta gerar provas para lógicas proposicional e de predicado.