Lógica Computacional

Licenciatura em Ciências da Computação - 2º ano

Tópicos

Avisos

Notícias

Já estão disponíveis os resultados dos exames de recurso, e Notas Finais.

-- MariaJoaoFrade - 03 Mar 2005

AVISO Sessão de Dúvidas

Na próxima 3ª feira (dia 15 Fev) às 17:00 no Lab 011, vai realizar-se uma sessão de esclarecimento de dúvidas.

-- MariaJoaoFrade - 10 Feb 2005

AVISO PROVAS ORAIS

As provas orais irão realizar-se na 2ª feira dia 14, pelas 15:00, na sala DI-A1.

-- MariaJoaoFrade - 10 Feb 2005

Os resultados dos exames da 1ª e 2ª chamadas já estão disponíveis.

-- MariaJoaoFrade - 10 Feb 2005

As Notas Práticas já estão disponíveis.

-- MariaJoaoFrade - 10 Jan 2005

A entrega de trabalhos será no dia 6 Jan 2005, 5ª feira. Está na recepção do DI a folha com os horários disponíveis, para os alunos se inscreverem.

-- MariaJoaoFrade - 13 Dec 2004

Já está disponível o enunciado do trabalho prático.

-- MariaJoaoFrade - 18 Nov. 2004

A inscrição nos turnos decorre no dia 23 Setembro (DI 0.11) no periodo das aulas teórico-práticas.

-- MariaJoaoFrade - 21 Set. 2004

Elementos Lógicos da Programação I

_Licenciatura em Matemática e Ciências da Computação_
2º Ano - 1º Semestre
Ano lectivo 2004/2005


Programa

  1. Dedução em Lógica Proposicional.
  2. Sistemas de Dedução Hilbertianos.
  3. Sistemas de Dedução de Gentzen e de Dedução Natural em LP.
  4. Dedução Automática em Lógica Proposicional.
  5. Sistemas Tableaux em LP.
  6. Método de Davis-Putman.
  7. Dedução em Lógica de Primeira Ordem.
  8. Sistemas de Dedução de Gentzen e de Dedução Natural em LPO.
  9. Tableaux na LPO.
  10. Introdução à Lógica Modal.
  11. Introdução à Lógica Linear.

Bibliografia

As notas acessíveis a partir desta página constituem o apoio documental base da disciplina e são complementadas pelos seguintes textos:

  • Basic Proof Theory. A.S. Troelstra & H.Schwichtenberg, Cambridge Tracks in Theoretical Computer Science, nº 48, 1996.

  • Proof Theory and Automated Deduction. Jean Goubault-Larrecq & Ian Mackie , Kluwer Academic Publishers, 1997.

  • First Order Logic and Automated Theorem Proving. Melvin Fitting, Graduate Texts in Computer Science. Springer-Verlag, 1996.

Critérios de Avaliação

A avaliação tem uma componente teórica e uma componente prática, ambas obrigatórias. A nota final será calculada com base na seguinte fórmula:

Nota Final = NT * 0.7 + NP * 0.3

sendo

  • NT a nota teórica (nota mínima de 9 valores), obtida através da realização de uma prova individual escrita;

  • NP a nota prática (nota mínima de 9 valores), resultante da avaliação de um trabalho prático (realizado em grupos de 3 alunos) e da avaliação contínua realizada ao longo das aulas laboratoriais e que terá por base a resolução de fichas de trabalho;

Equipa Docente

Horário Lectivo

  Horário Sala Docente
Teórica 3ªfeira 8:00-9:00 CP3.101 jmv
Teórica 5ªfeira 15:00-16:00 CP2.303 jmv
Turnos Horário Sala Docente
TP1 5ªfeira 9:00-11:00 DI 0.11 mjf
TP2 5ªfeira 16:00-18:00 DI 0.11 mjf

Horário de Atendimento

Docente Horário
jmv  
mjf 2ªfeira 12:00-13:00 e 14:00-18:00

Material Disponibilizado

Aulas Teóricas

Aulas Práticas

Fichas de trabalho

Isabelle/Isar

  • Exemplos de utilização do Isar (pdf) (ps)
  • Dedução Natural para a Lógica Proposicional (DNLP.thy)
  • Cálculo de Sequentes para a Lógica Proposicional Clássica (LKLP.thy)
  • Dedução Natural para a Lógica de Primeira Ordem (DNFOL.thy)
  • Cálculo de Sequentes para a Lógica de Primeira Ordem Clássica (LKFOL.thy)

Trabalho Prático

Exames 2004

Exames 2005

Links Úteis

Notas

Notas 2005/06

r25 - 26 Feb 2007 - 00:55:53 - JoseBacelarAlmeida
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM