Lógica para Computação - Sistemas Computacionais de Auxílio ao Aprendizado de Lógica

Edição de 13h53min de 29 de outubro de 2010

Simuladores de lógica digital

• TkGate
  • Roda em Linux! Testado no Fedora 11 por Adolfo Neto

• KSimus
  • Descrição em http://www.linuxjournal.com/content/digital-and-analog-circuit-simulation-ksimus

Para diversos métodos relacionados à lógica proposicional

• NICOLADELLI, José Martim. ASA-CalcPro. Disponível em: <http://www.asacalcpro.com.br>. Acesso em: 17 fev. 2009.
  • Vínculo direto para o download do programa: http://www.asacalcpro.com.br/asa.exe
• Logicamente: http://www.dimap.ufrn.br/logicamente/

Tablôs

• NICOLADELLI, José Martim. ASA-Tableaux. Disponível em: <http://www.asacalcpro.com.br>. Acesso em: 09 dez. 2008.
  • Vínculo direto para o download do programa: http://www.asacalcpro.com.br/InstallTableaux/ASA-Tableaux.exe

• Método dos tableaux analíticos em LISP: http://www.dainf.ct.utfpr.edu.br/~kaestner/Logica/tableau-method.lsp.

• WDTP - Wagner Dias Tableau Prover (para tablôs analíticos e tablôs KE)

• Tree Proof Generator, by Wolfgang Schwarz - um demonstrador de teoremas online baseado em tablôs analíticos (árvores de prova) para lógicas clássica proposicional e de predicados.

Tablôs KE

• ENDRISS, Ulle. WinKE: A Proof Assistant for Teaching Logic. Disponível em: <http://staff.science.uva.nl/~ulle/WinKE/>. Acesso em: 12 dez. 2008.

• NETO, Adolfo. KEMS: Um provador de teoremas multi-estratégia baseado no método KE. Disponível em: <http://www.dainf.ct.utfpr.edu.br/~adolfo/KEMS>. Acesso em: 12 dez. 2008.

Dedução Natural

• JAPE. Disponível em: <http://jape.org.uk>. Acesso em: 19 ago. 2009.
  • Ver instruções (desatualizadas) em português neste link: http://www.cos.ufrj.br/~mario/logica/jape.htm

• BRODA, K.;EISENBACH, S.; KHOSHNEVISAN, H.; VICKERS, S. Pandora: Proof Assistant for Natural Deduction using Organised Rectangular Areas. Disponível em: <http://www.doc.ic.ac.uk/pandora/>. Acesso em: 15 dez. 2008.
  • A learning support tool designed to guide the construction of natural deduction proofs.

Tabelas-verdade

• Construtor de tabelas-verdade: Java applet
• http://turner.faculty.swau.edu/mathematics/materialslibrary/truth/
• http://www.math.csusb.edu/notes/quizzes/tablequiz/tablepractice.html
• http://www-cs-students.stanford.edu/~silver//truth/
• http://en.wikipedia.org/wiki/Truth_table
• GOTTSCHALL, Christian. Gateway to Logic. Disponível em:<http://logik.phl.univie.ac.at/~chris/gateway/formular-uk.html>. Acesso em: 12 mar. 2009.

Formas normais

• Applet para converter fórmulas para formas normais
• [http://github.com/adolfont/Logic-in-Computing/tree/master/Programming/Prolog/examples/logPropTool

Programas em Prolog (por Jomi Fred Hübner) para diversas tarefas, entre os quais um (transform.pl) para conversão para forma normal conjuntiva]

• • Para executar o conversor de fórmulas para Forma Normal Conjuntiva, baixe os dois arquivos abaixo e consulte tranform ("consult(tranform)") no SWI Prolog:
    • http://github.com/adolfont/Logic-in-Computing/blob/master/Programming/Prolog/examples/logPropTool/transform.pl
    • http://github.com/adolfont/Logic-in-Computing/blob/master/Programming/Prolog/examples/logPropTool/truthTable.pl
• Wolphram Alpha http://www.wolframalpha.com
  • Exemplo de uso do Wolphram Alpha: http://www.wolframalpha.com/input/?i=+(a+%26+b)+%7C+(c+%26+d+%26+~e)
• Formas Normais em Lua
  • Versão incompleta: http://github.com/adolfont/logic-in-lua/blob/master/nf.lua
  • Lua online: http://www.lua.org/cgi-bin/demo

Lógica de Predicados

• Tarski's World:
  • http://ggww2.stanford.edu/GUS/tarskisworld/index.jsp

Programação em Lógica

• Interpretador SWI-Prolog:
  • http://www.swi-prolog.org/

Outras linguagens de programação utilizadas para programação de sistemas lógicos

• Linguagem CLISP: http://clisp.cons.org/ (freeware).
• Python: http://www.python.org/

Algoritmo de Wang

• Algoritmo de Wang em LISP: http://www.cse.buffalo.edu/~shapiro/Reasoning/wang.html.

Resolução

• SHAPIRO, Stuart C. Procedimento de Resolução em LISP: http://www.cse.buffalo.edu/~shapiro/Reasoning/resolution.html (ou ainda sem packages em http://www.dainf.ct.utfpr.edu.br/~kaestner/Logica/resolution-method.lsp).

A organizar

• Provador de teoremas YACAS:
  • http://yacas.sourceforge.net/
    • um sistema geral para computar sistemas lógicos (freeware em Applet Java)
    • an easy to use, general purpose Computer Algebra System, a program for symbolic manipulation of mathematical expressions.

• Software para iPhone/iPod

Listas de sistemas

• Tools for logic in computer science
• Logic software and logic education, list maintained by Hans van Ditmarsch