2006.2 - DIM0099 - Tópicos Especiais em Computação X

*LÓGICA COMPUTACIONAL: demonstração assistida e semi-automática de teoremas*

Professor: João Marcos

Créditos: 4 Horário: 46M34 Sala: 3D5

Pré-requisitos: não há

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)