EQUIPA DOCENTE (98/99)

• Simão Melo de Sousa

A presente disciplina de Lógica é uma disciplina comum aos cursos de Matemática Ensino e  Matemática/Informática. Trata-se da primeira e única cadeira na área da Lógica de ambos os cursos. Trata-se também de uma disciplina leccionada a duas assistências com objectivos e culturas de aparência diferente. Por isso, a abordagem escolhida tem como principal objectivo a introdução dos conceitos básicos de forma a apresentar a Lógica como uma área de comum interesse a essas duas assistências.

Atingir este objectivo geral  divide a aprendizagem em várias metas intermediárias e complementares

1. Tentamos numa primeira fase definir, explorar e relacionar as noções de verdade e de validade através da semântica e sintaxe dos formalismos lógicos tradicionais. Um cuidado particular é dado à noção de dedução e da sua sistematização. Para esse efeito, ao detrimento de outros formalismos, apresentamos um formalismo conhecido pelas suas boas propriedades didácticas: a Dedução Natural.
2. Esta primeira abordagem computacional da lógica dá naturalmente sequência à segunda parte da disciplina que tenta definir o conceito de cálculo efectivo, ou seja da capacidade de um problema ter ou não uma solução sistemática, de uma função ser ou não computável. Apresentamos neste intuinto o formalismo das funções recursivas de Kleene, preferido à abordagem clássica pelas máquinas de Turing.
3. A última parte da disciplina é dedicada a um formalismo, o lambda-cálculo, que permite de forma inequívoca juntar as duas assistências pelas boas propriedades inerente ao cálculo: O lambda-cálculo é um formalismo computacional elegante suficientemente poderoso  para ser uma completa linguagem de programação que permite representar tanto lógicas, através por exemplo da codificação da dedução natural,  como também todas as funções computáveis. Atingimos assim a meta principal concluindo que, afinal, demonstrar pode ser programar.

A  avaliação será realizada alternativamente:

• por Frequência
• por Exame

Em que a nota prática representa a soma da nota atribuída a um trabalho realizado em grupo com a nota atribuída à resolução individual  de exercícios entregues à equipa docente.

A nota do exame será determinada exclusivamente por uma prova escrita
 
 

TRABALHOS

A lista dos trabalhos que contam para a nota prática da frequência encontra-se Aqui.

PROGRAMA RESUMIDO

• Introdução à Induçao Estrutural
• Indução Estrutural
• Termos
• Funções definidas por Indução
• Lógica Proposicional
• Sintaxe
• Semântica
• Sistemas Completos e Formas Normais
• Consequência Semântica e Compacidade
• Lógica de Primeira Ordem
• Sintaxe
• Semântica
• Formas Normais e Transformações
• Consequência Semântica e Compacidade
• Sistemas de Dedução e Demonstrações Formais
• Dedução Natural e Consequência Sintáctica
• Propriedades, correcção e completude da Dedução Natural
• Computabilidade
• Funções Primitivas Recursivas
• Funções Recursivas
• Computabilidade e Decidibilidade
• Indecidibilidade e Incompletude
• Lambda-Cálculo
• Lambda-Termos, Redução e Propriedades
• Computabilidade e Funções Lambda Definíveis
• Lambda-Cálculo Simplesmente Tipado
• Representação da Lógica

• A. Arnold I. Guessarian. Mathématique pour l'Informatique. Masson, terceira edição, 1997.
• H. Barendregt. Lambda Calculi with Types. Handbook of Logic In Computer Science, Vol. 2, Oxford University Press, 1992
• D. Cohen. Computability and logic. John Wiley and Son, primeira edição, 1987.
• R. Cori e D. Lascar. Logique mathématique, Volume 1 e 2. Masson, primeira edição, 1993.
• H.B. Enderton. A Mathematical Introduction to Logic. Academic Press, primeira edição, 1972.
• P. Fejer e D. Simovici. Mathematical Foundations of Computer Science. Springer Verlag, primeira edição, 1990.
• C. Hankin. Lambda-calculi. A guide for computer scientist. Oxford University Press, 1994.
• R. Lassaigne e M. de Rougemont. Logique et fondements de l'informatique. Hermès, 1993.
• W. Kneale e M. Kneale. O Desenvolvimento da Lógica. Fundação Calouste Gulbenkian, terceira edição (1962)1991.
• A.S. Troelstra. Basic Proof Theory. Cambridge University Press, 1996.
• D. Van Dalen. Logic and Structure. Springer Verlag, terceira edição, 1997.
• P. Wolper. Introduction à la calculabilité. InterEdition, Masson, 1991.
• Ver a bibliografia "online" exposta na secção seguinte.

Uma cópia da "coleção" de acetatos usados nas aulas (téoricas e práticas) está disponível. Consulte regularmente a reprografia preferida por vocês.
O Sistema ALFIE é um sistema computacional on-line (i.e. accessível  e executável na Web)  que permite correr a Dedução Natural na lógica proposicional. Experimentem!
A linguagem Haskell é uma linguagem funcional (i.e. baseada no lambda-cálculo) freeware e diponível on-line. Além de ser uma linguagem de programação, ela permite pôr em prática os conceitos introduzidos no capítulo sobre a indução. Experimentem!

Práticas e exercícios para resolver:
    Aqui vai a primeira ficha prática da diciplina (contem o primeiro exercício para resolver).
    Aqui vai a segunda ficha prática da diciplina.
    Aqui vai o segundo exercício para resolver da diciplina (entrega 23 de Novembro 98).
    Aqui vai o terceiro exercício para resolver da diciplina (entrega 4 de Janeiro 99).
    Aqui vai o quarto exercício para resolver da diciplina (entrega 20 de Janeiro 99).

Vários textos disponíveis online tratam de partes ou da totalidade da materia exposta nesta disciplina. Eis aqui alguns exemplos (formato postscript)

• Uma referência completa e extensa: 1(M.H.Sorensen e P.Urzyczyn, DIKU)
• Lógica e Dedução: 1(Valença, U.Minho), 2(Broda, U.Porto), 3(Broda, U.Porto)
• Lógica e Decidibilidade: 1(Broda, U.Porto)
• Lambda cálculo: 1(Valença, U.Minho), 2(Paulson, Cambridge), 3(Gordon, Cambridge),  4(Meunier, Connecticut), 5(Huet, INRIA), 6(Barendregt,KUN)
• Complementos teóricos em reescrita: 1(Barros, U.Minho) 2(Bognar, CWI) 3(Klop-V.Oostrom-V.Raamsdonk, CWI)


Para ver e imprimir os ficheiros em formato postscript em Windows utilize o Ghostview e o Ghostscript

HORÁRIO DE ATENDIMENTO
 

Enviar comentários e dúvidas para : desousa@noe.ubi.pt