*LÓGICA COMPUTACIONAL: demonstração assistida e semi-automática de teoremas*
EMENTA
Efetuar demonstrações em sistemas de dedução natural para as lógicas clássica proposicional e de primeira ordem, e para várias lógicas modais. Estudar a sintaxe, a semântica e alguns metateoremas destas lógicas. Codificar usando uma ferramenta computacional (Isabelle) de apoio à demonstração os sistemas de dedução natural e de sequentes destas lógicas, bem como de novas lógicas não-clássicas. Utilizar a ferramenta para efetuar demonstrações assistidas e automáticas.
BIBLIOGRAFIA
* D. van Dalen. Logic and Structure. Springer-Verlag, 1994.
* P. Gouveia, F.M. Dionísio, J. Marcos. Lógica Computacional. DMIST, 2000.
* L. C. Paulson. Isabelle: A Generic Theorem Prover. Springer Verlag, LNCS 828, 1994.
* L. C. Paulson. Introduction to Isabelle. University of Cambridge, 1999.
* A. Troelstra, H. Schwichtenberg. Basic Proof Theory. Cambridge University Press, 2000.
* L. Viganò. Labelled Non-Classical Logics. Kluwer Academic Publishers, 2000.
PRINCIPAL: Livro "Lógica Computacional"
- Capítulo 1: Lógica Clássica Proposicional (LCP) -> 116 páginas
- Capítulo 2: Representação de LCP na ferramenta Isabelle -> 105 páginas
- Capítulo 3 (versão 1 e versão 2): Lógica Clássica de Primeira Ordem (LCPO) -> 86 páginas (só teoria) + 83 páginas (teoria + Isabelle)
- Capítulo 4: Lógica Modal (LM) -> 130 páginas (teoria + Isabelle)