Lógica Computacional

Disciplina da Secção de Lógica e Computação.

Cursos:
LCI (Licenciatura em Ciências Informáticas). Ano: 2. Semestre: 1.
LMAC (Licenciatura em Matemática e Computação). Ano: 3. Semestre: 1.

Professores Responsáveis: Francisco Miguel Dionísio.

Semestre corrente: AVISOS e outras informações.

Objectivos

Efectuar provas em sistemas de dedução natural para as lógicas proposicional, clássica e várias lógicas modais. Codificar usando uma ferramenta de apoio à prova os sistemas de dedução natural destas lógicas, bem como de novas lógicas. Utilizar a ferramenta para efectuar provas.

Programa

Importância da Lógica em Engenharia da Programação e Inteligência Artificial. Dedução natural em lógica proposicional. Iniciação ao sistema Isabelle. Codificação em Isabelle. Elementos de lógica de primeira ordem: sintaxe, semântica e dedução natural. Alguns metateoremas. Codificação em Isabelle. Elementos de lógica modal proposicional: sintaxe, semântica e dedução natural etiquetada para diferentes sistemas modais. Alguns metateoremas. Codificação em Isabelle.

Bibliografia básica

• P. Gouveia e F.M. Dionísio. Lógica Computacional.
  DMIST, 2000.

Bibliografia complementar

• D. van Dalen. Logic and Structure (terceira edição).
  Springer-Verlag, 1994.
• 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 e H. Schwichtenberg. Basic Proof Theory (segunda edição).
  Cambridge University Press, 2000.
• L. Viganò. Labelled Non-Classical Logics.
  Kluwer Academic Publishers, 2000.

Avaliação

Componente teórica: exame final (ou 2 testes) (50%). Componente prática: projecto (50%).

Carga horária semanal

Aulas teóricas: 3h. Aulas práticas: 2h. Estudo recomendado: 4h.

Última actualização: 26 de Fevereiro de 2003.