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

Bibliografia complementar

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.