Lógica para Computação

De Wiki DAINF
(Diferença entre revisões)
(Bibliografia)
(Sistemas Computacionais de Auxílio ao Aprendizado de Lógica)
Linha 100: Linha 100:
 
== Sistemas Computacionais de Auxílio ao Aprendizado de Lógica ==
 
== Sistemas Computacionais de Auxílio ao Aprendizado de Lógica ==
  
=== Simuladores de lógica digital ===
+
[[Lógica para Computação - Sistemas Computacionais de Auxílio ao Aprendizado de Lógica | Sistemas Computacionais de Auxílio ao Aprendizado de Lógica]
 
+
* [http://www.tkgate.org/ TkGate]
+
** Roda em Linux! Testado no Fedora 11 por [[Adolfo Neto]]
+
 
+
* [http://ksimus.berlios.de/ 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)
+
 
+
* [http://www.umsu.de/logik/trees/ 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 ===
+
 
+
* [http://www.brian-borowski.com/Truth/ 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 ===
+
 
+
* [http://www.izyt.com/BooleanLogic/applet.php Applet para converter fórmulas para formas normais]
+
* [http://bit.ly/9eEoEt Programas em Prolog (por Jomi Fred Hübner) para diversas tarefas, entre os quais um (transform.pl) para conversão para forma normal conjuntiva]
+
 
+
=== 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.''
+
 
+
* [http://www.ucalgary.ca/~rzach/logblog/2009/09/logic-on-your-iphone.html Software para iPhone/iPod]
+
 
+
=== Listas de sistemas ===
+
 
+
* [http://www.icetcs.ru.is/luca/courses/LOGIC/tools.html Tools for logic in computer science]
+
* [http://www.cs.otago.ac.nz/staffpriv/hans/logiccourseware.html Logic software and logic education, list maintained by Hans van Ditmarsch]
+
 
+
  
 
=== Exemplos de especificação formal ===
 
=== Exemplos de especificação formal ===

Edição de 16h57min de 5 de agosto de 2010

Tabela de conteúdo

Informações Gerais


Objetivos da disciplina

Os objetivos da disciplina Lógica para Computação são "desenvolver conceitos de lógica proposicional e de predicados, prova automática de teoremas e programação em lógica".

O papel desta disciplina é o de mostrar como uma lógica pode ser vista como uma linguagem de especificação tanto de sistemas como de suas propriedades.

Sendo assim, pode-se entender a disciplina como o estudo das lógicas proposicional e predicativa do ponto de vista da verificação de propriedades por elas expressas, permitindo que o aluno seja capaz de identificar o tipo de lógica que pode ser usada para especificar um sistema ou propriedade, bem como realizar a modelagem de sistemas e propriedades por meio da lógica escolhida.

Bibliografia

Bibliografia Básica

  • HUTH, Michael; RYAN, Michael. Lógica em Ciência da Computação: modelagem e argumentação sobre sistemas. Segunda edição. Editora LTC: 2008. 326 p.
    • Tradução de:
      • HUTH, Michael; RYAN, Michael. Logic in Computer Science: modelling and reasoning about systems. Segunda edição. Cambridge University Press: 2004. 427 p.
      • Página do livro original (contém errata): http://www.cs.bham.ac.uk/research/projects/lics/

Bibliografia Complementar

Alguns slides

Referências

Vídeos

Links Diversos

Lógica de Predicados

Links interesssantes:

Material Adicional

Porque estudar lógica

Programação em Lógica

Sistemas Computacionais de Auxílio ao Aprendizado de Lógica

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

Exemplos de especificação formal

Razões para Estudar Lógica

Ferramentas pessoais