FERNANDO FERREIRA FERNANDO FERREIRA A primeira aula teórica é no dia 27 de Fevereiro. As aulas teórico-práticas começam na semana seguinte.
Matéria:
Introdução às linguagens da lógica de primeira ordem com igualdade, desde o cálculo proposicional até ao cálculo de predicados. Em cada etapa estudam-se os aspectos sintácticos e semânticos e os métodos de demonstração associados ao fragmento em causa. É dada ênfase à noção semântica de consequência lógica e sua formalização através dum cálculo dedutivo. Cálculo proposicional: constantes, símbolos relacionais (predicados), símbolos funcionais, termos, igualdade, sentenças atómicas; exemplos: as linguagens da teoria de conjuntos e da aritmética; métodos de demonstração; conectivos lógicos, sentenças, equivalência, satisfação e tautologias, deduções formais, formas normais conjuntivas e disjuntivas. Discussão informal da completude proposicional do cálculo de dedução formal apresentado. Sentenças de Horn e o algoritmo (eficiente) de satisfação para sentenças de Horn. Cálculo de predicados: variáveis, fórmulas atómicas, quantificadores, fórmulas e sentenças, semântica; uso de quantificadores múltiplos, equivalência lógica e deduções formais envolvendo quantificadores; forma prenexa normal. Acerca do cálculo de dedução formal estudado.
Pode também consultar a página da disciplina do ano passado aqui.
Livro vivamente recomendado: “Language, Proof and Logic” de Jon Barwise e John Etchemendy. As aulas vão seguir fielmente este livro do capítulo 1 ao capítulo 13. Incluem-se também as secções 1 e 3 do capítulo 17.
Pode obter informações sobre este livro aqui. O livro encontra-se à venda na livraria do campus e está disponível na Biblioteca da Universidade. Pode aceder-se ao Catálogo Colectivo das Bibliotecas da Universidade de Lisboa aqui.
Deve obter na reprografia do Departamento de Informática a primeira parte dos exercícios das aulas teórico-práticas. Estes exercícios devem ser levados para as aulas teórico-práticas. A segunda parte dos exercícios estará disponível a seu devido tempo (anunciado na aula teórica).
Os mundos que constam dos exercícios podem também ser descarregados aqui: Mundo de Bolzano, Mundo de Boole, Mundo de Leibniz, Mundo de Lestrade, Mundo de Montague, Mundo de Ramsey, Mundo de Sherlock, Mundo de Wittgenstein. Existem novos mundos para a segunda parte dos exercícios. São eles: Mundo de Carroll, Mundo de Maigret, Mundo de Peano, Mundo de Peirce e Mundo de Reichenbach.
Fernando Ferreira:
Gabinete 6.2.8 do edifício C6 da Faculdade de Ciências da Universidade de Lisboa.
Telefone: 217500294.
Endereço de correio electrónico: ferferr@cii.fc.ul.pt. Quando me contactar por correio electrónico escreva “LPO2007” (não inclua as aspas) no campo do subject.
Terça-feira e quinta-feira das 12h às 13h. Sala: C8.2.47.
Horário de atendimento da aula teórica: terças-feiras das 13h às 14h (no gabinete 6.2.8).
Dois testes intermédios in situ na aula teórica, nos dias 17 de Abril e 17 de Maio. Os testes são obrigatórios e valem 20% da nota final. Os restantes 80% são objecto de exame final escrito durante a época regular de exames. O Professor reserva-se o direito de efectuar exame oral a um aluno se o considerar necessário.
Enunciado e solução do primeiro teste: aqui com os Mundo A, Mundo B e Mundo C e a dedução formal do exercício quatro.
Enunciado e solução do segundo teste: aqui com os Mundo A, Mundo B e Mundo C e a dedução formal do exercício quatro.
Enunciado e solução do primeiro exame (21 de Junho de 2007): aqui com os Mundo A, Mundo B e Mundo C, o contra-exemplo para o exercício III e as deduções formais dos exercícios IX, X e XI.
Enunciado do exame de segunda época está aqui: aqui, com os Mundo A, Mundo B e Mundo C.
AULA 1 [27/2] Apresentação. Nomes e símbolos predicativos (e suas aridades). Sentenças atómicas. Verdade e falsidade de sentenças atómicas interpretadas. A linguagem do mundo de blocos.
AULA 2 [1/3] Linguagens de primeira-ordem em geral. Símbolos funcionais. A linguagem da teoria dos conjuntos. A linguagem da aritmética. Definição indutiva dos termos da linguagem da aritmética.
AULA 3 [6/3] Primeira abordagem à noção (semântica) de consequência lógica. A noção de contra-exemplo. Inferências dado o significado dos símbolos da linguagem. Inferências da lógica de primeira-ordem com igualdade: regras de introdução e eliminação da igualdade. O sistema formal de Fitch. Demonstração informal e formal da lei de simetria da igualdade.
AULA 4 [8/3] Os conectivos Booleanos da negação, conjunção e disjunção. Lei da dupla negação e leis de De Morgan. Digressão sobre a disjunção exclusiva e tabelas de verdade. Ambiguidade e parêntesis.
AULA 5 [13/3] Tautologias, satisfação tautológica, contradição tautológica, consequência tautológica, equivalência tautológica. Leis associativas, comutativas e de idempotência da conjunção e da disjunção. Leis distributivas.
AULA 6 [15/3] Leis da absorção. Formas normais negativas, conjuntivas e disjuntivas. Métodos de demonstração: introdução e eliminação da conjunção; introdução da disjunção.
AULA 7 [20/3] Demonstração por casos. Exemplos. Demonstração por contradição (reductio ad absurdum). O símbolo da contradição.
AULA 8 [22/3] A demonstração por contradição de que a raíz quadrada de 2 é um número irracional. Regras de dedução de Fitch para a conjunção e a disjunção. Exemplo.
AULA 9 [27/3] Regras de dedução de Fitch para a negação e para o símbolo de contradição. Exemplos de deduções, estratégias dedutivas, etc.
AULA 10 [29/3] Continuação da aula anterior. O condicional (implicação) e o bicondicional (equivalência) e a sua semântica de valores de verdade. Questões de tradução.
AULA 11 [3/4] Completude vero-funcional. Introdução às demonstrações com o símbolo do condicional.
AULA 12 [12/4] Demonstrações formais e informais com o símbolo do condicional. Regras de introdução e eliminação para este conectivo (e para o bicondicional). Exemplos de demonstrações no sistema de Fitch.
AULA 13 [17/4] Teste intermédio.
AULA 14 [19/4] Enunciados dos teoremas da Adequação (Soundness) e Completude (Completeness) para o cálculo proposicional. Valorações Booleanas. Noções e resultados básicos.
AULA 15 [24/4] Sentenças de Horn. Forma implicativa das sentenças de Horn. O algoritmo da satisfação para sentenças de Horn.
AULA 16 [26/4] Introdução à quantificação. Variáveis, variáveis mudas. Fórmulas vs sentenças. Semântica informal dos quantificadores (universal e existencial). As quatro formas aristotélicas.
AULA 17 [3/5] Satisfação duma fórmula por objectos do domínio. Algumas traduções. Generalizações vácuas e inerentemente vácuas. Implicatura conversacional. Quantificações e símbolos funcionais. Notações alternativas.
AULA 18 [8/5] Por que razão se diz lógica de primeira ordem? A noção de validade de primeira ordem e de consequência de primeira ordem. Exemplos. Tautologias na lógica de primeira ordem.
AULA 19 [10/5] Forma proposicional (truth-functional form) duma sentença da linguagem da lógica de primeira-ordem. Algoritmo para encontrar a forma proposicional. Equivalências com quantificadores: as leis de De Morgan generalizadas (aplicação ao quadrado de oposição aristotélico) e outras equivalências importantes. Introdução à quantificação múltipla.
AULA 20 [15/5] A importância da ordem dos quantificadores. Traduções da linguagem natural para a linguagem de LPO: tradução passo-a-passo, paráfrases, ambiguidade. Forma prenexa.
AULA 21 [17/5] Teste intermédio.
AULA 22 [22/5] Passos algorítmicos para chegar à forma prenexa. Exemplos. Introdução às demonstrações informais com quantificadores. As leis da instanciação universal e da generalização existencial.
AULA 23 [24/5] Continuação do tópico das demonstrações informais com quantificadores. O método da demonstração condicional geral e as leis da generalização universal e da instanciação existencial. Exemplos.
AULA 24 [29/5] Quantificações múltiplas. Regras formais para a quantificação universal: eliminação e introdução (duas versões). Exemplo.
AULA 24 [31/5] Regras formais para a quantificação existencial: eliminação e introdução. Exemplos.
AULA 25 [5/6] Mais exemplos de demonstrações formais. THE END.