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
- Dedução em Lógica Proposicional.
- Sistemas de Dedução Hilbertianos.
- Sistemas de Dedução de Gentzen e de Dedução Natural em LP.
- Dedução Automática em Lógica Proposicional.
- Sistemas Tableaux em LP.
- Método de Davis-Putman.
- Dedução em Lógica de Primeira Ordem.
- Sistemas de Dedução de Gentzen e de Dedução Natural em LPO.
- Tableaux na LPO.
- Introdução à Lógica Modal.
- 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
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