Lógica para Computação - Sistemas Computacionais de Auxílio ao Aprendizado de Lógica
De Wiki DAINF
(Diferença entre revisões)
(→Formas normais) |
(→Formas normais) |
||
| Linha 54: | Linha 54: | ||
* Wolphram Alpha http://www.wolframalpha.com | * Wolphram Alpha http://www.wolframalpha.com | ||
** Exemplo de uso do Wolphram Alpha: http://www.wolframalpha.com/input/?i=+(a+%26+b)+|+(c+%26+d+%26+~e) | ** Exemplo de uso do Wolphram Alpha: http://www.wolframalpha.com/input/?i=+(a+%26+b)+|+(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 === | === Lógica de Predicados === | ||
Edição de 12h25min de 27 de outubro de 2010
Tabela de conteúdo |
Simuladores de lógica digital
- TkGate
- Roda em Linux! Testado no Fedora 11 por Adolfo Neto
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
- Programas em Prolog (por Jomi Fred Hübner) para diversas tarefas, entre os quais um (transform.pl) para conversão para forma normal conjuntiva
- 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:
Programação em Lógica
- Interpretador SWI-Prolog:
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.
- http://yacas.sourceforge.net/
